let A1, A2 be Subset of F₁(); :: thesis: ( ( for x being set holds
( x in A1 iff P₁[x] ) ) & ( for x being set holds
( x in A2 iff P₁[x] ) ) implies A1 = A2 )
assume that
A1: for x being set holds
( x in A1 iff P₁[x] ) and
A2: for x being set holds
( x in A2 iff P₁[x] ) ; :: thesis: A1 = A2
thus A1 c= A2 :: according to XBOOLE_0:def 10 :: thesis: A2 c= A1

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A1 or x in A2 )
assume x in A1 ; :: thesis: x in A2
then P₁[x] by A1;
hence x in A2 by A2; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A2 or x in A1 )
assume x in A2 ; :: thesis: x in A1
then P₁[x] by A2;
hence x in A1 by A1; :: thesis: verum