% Mizar problem: s11_schems_1,schems_1,170,12 
include('Axioms/SET010^0.ax').
thf(p1_s11_schems_1_type,type,( p1_s11_schems_1: $i > $o )).
thf(p2_s11_schems_1_type,type,( p2_s11_schems_1: $i > $o )).
thf(s10_schems_1,axiom,( ! [A: $i > $o] : ! [B: $i > $o] : ( ! [C: $i] : ? [D: $i] : ( ( B @ D ) & ( A @ C ) ) => ( ? [C: $i] : ( B @ C ) & ! [C: $i] : ( A @ C ) ) ) ),file(schems_1,s10_schems_1)).
thf(s11_schems_1,conjecture,( ! [A: $i] : ? [B: $i] : ( ( p1_s11_schems_1 @ B ) & ( p2_s11_schems_1 @ A ) ) => ? [A: $i] : ! [B: $i] : ( ( p1_s11_schems_1 @ A ) & ( p2_s11_schems_1 @ B ) ) ),file(schems_1,s11_schems_1)).
