let P, Q be preBoolean set ; :: thesis:
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:
for x being object holds
( x in P iff x in Q )

let x be object ; :: thesis:
reconsider xx = x as set by TARSKI:1;
thus ( x in P implies x in Q ) :: thesis:

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

end;

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

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

end;