let A, B be Subset of ; :: thesis: ( ( for p being Point of holds
( p in A iff P₁[p] ) ) & ( for p being Point of holds
( p in B iff P₁[p] ) ) implies A = B )
assume that
A1: for p being Point of holds
( p in A iff P₁[p] ) and
A2: for p being Point of holds
( p in B iff P₁[p] ) ; :: thesis: A = B

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: B c= A

let x be set ; :: thesis: ( x in A implies x in B )
assume A3: x in A ; :: thesis: x in B
then P₁[x] by A1;
hence x in B by A2, A3; :: thesis: verum

end;

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