defpred S₁[ set ] means ( $1 in 4C_3 F & ex a, b, c, d being Element of [: the carrier of F, the carrier of F, the carrier of F:] st
( $1 = [a,b,c,d] & (((a `1_3) - (b `1_3)) * ((c `2_3) - (d `2_3))) - (((c `1_3) - (d `1_3)) * ((a `2_3) - (b `2_3))) = 0. F & (((a `1_3) - (b `1_3)) * ((c `3_3) - (d `3_3))) - (((c `1_3) - (d `1_3)) * ((a `3_3) - (b `3_3))) = 0. F & (((a `2_3) - (b `2_3)) * ((c `3_3) - (d `3_3))) - (((c `2_3) - (d `2_3)) * ((a `3_3) - (b `3_3))) = 0. F ) );
let H1, H2 be set ; :: thesis: ( ( for x being set holds
( x in H1 iff ( x in 4C_3 F & ex a, b, c, d being Element of [: the carrier of F, the carrier of F, the carrier of F:] st
( x = [a,b,c,d] & (((a `1_3) - (b `1_3)) * ((c `2_3) - (d `2_3))) - (((c `1_3) - (d `1_3)) * ((a `2_3) - (b `2_3))) = 0. F & (((a `1_3) - (b `1_3)) * ((c `3_3) - (d `3_3))) - (((c `1_3) - (d `1_3)) * ((a `3_3) - (b `3_3))) = 0. F & (((a `2_3) - (b `2_3)) * ((c `3_3) - (d `3_3))) - (((c `2_3) - (d `2_3)) * ((a `3_3) - (b `3_3))) = 0. F ) ) ) ) & ( for x being set holds
( x in H2 iff ( x in 4C_3 F & ex a, b, c, d being Element of [: the carrier of F, the carrier of F, the carrier of F:] st
( x = [a,b,c,d] & (((a `1_3) - (b `1_3)) * ((c `2_3) - (d `2_3))) - (((c `1_3) - (d `1_3)) * ((a `2_3) - (b `2_3))) = 0. F & (((a `1_3) - (b `1_3)) * ((c `3_3) - (d `3_3))) - (((c `1_3) - (d `1_3)) * ((a `3_3) - (b `3_3))) = 0. F & (((a `2_3) - (b `2_3)) * ((c `3_3) - (d `3_3))) - (((c `2_3) - (d `2_3)) * ((a `3_3) - (b `3_3))) = 0. F ) ) ) ) implies H1 = H2 )
assume that
A1: for x being set holds
( x in H1 iff S₁[x] ) and
A2: for x being set holds
( x in H2 iff S₁[x] ) ; :: thesis: H1 = H2
for x being set holds
( x in H1 iff x in H2 )

proof

let x be set ; :: thesis: ( x in H1 iff x in H2 )
( x in H1 iff S₁[x] ) by A1;
hence ( x in H1 iff x in H2 ) by A2; :: thesis: verum

end;

hence H1 = H2 by TARSKI:1; :: thesis: verum