let A1, A2 be Subset of F₁(); :: thesis: ( ( for x being object holds
( x in A1 iff P₁[x] ) ) & ( for x being object holds
( x in A2 iff P₁[x] ) ) implies A1 = A2 )
assume that
A1: for x being object holds
( x in A1 iff P₁[x] ) and
A2: for x being object holds
( x in A2 iff P₁[x] ) ; :: thesis: A1 = A2
thus A1 c= A2 by A1, A2; :: according to XBOOLE_0:def 10 :: thesis: A2 c= A1
let x be object ; :: 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