let P, Q be preBoolean set ; :: thesis: ( ( for X being set holds
( X in P iff ( X c= A & X is finite ) ) ) & ( for X being set holds
( X in Q iff ( X c= A & X is finite ) ) ) implies P = Q )
assume that
A11: for X being set holds
( X in P iff ( X c= A & X is finite ) ) and
A12: for X being set holds
( X in Q iff ( X c= A & X is finite ) ) ; :: thesis: P = Q
for x being set holds
( x in P iff x in Q )

proof

let x be set ; :: thesis: ( x in P iff x in Q )
thus ( x in P implies x in Q ) :: thesis: ( x in Q implies x in P )

proof

assume x in P ; :: thesis: x in Q
then ( x c= A & x is finite ) by A11;
hence x in Q by A12; :: thesis: verum

end;

thus ( x in Q implies x in P ) :: thesis: verum

proof

assume x in Q ; :: thesis: x in P
then ( x c= A & x is finite ) by A12;
hence x in P by A11; :: thesis: verum

end;

end;

hence P = Q by TARSKI:1; :: thesis: verum