let Z1, Z2 be set ; :: thesis: ( ( X <> {} & ( for x being object holds

( x in Z1 iff for Y being set st Y in X holds

x in Y ) ) & ( for x being object holds

( x in Z2 iff for Y being set st Y in X holds

x in Y ) ) implies Z1 = Z2 ) & ( not X <> {} & Z1 = {} & Z2 = {} implies Z1 = Z2 ) )

( x in Z1 iff for Y being set st Y in X holds

x in Y ) ) & ( for x being object holds

( x in Z2 iff for Y being set st Y in X holds

x in Y ) ) implies Z1 = Z2 ) & ( not X <> {} & Z1 = {} & Z2 = {} implies Z1 = Z2 ) ) ; :: thesis: verum

( x in Z1 iff for Y being set st Y in X holds

x in Y ) ) & ( for x being object holds

( x in Z2 iff for Y being set st Y in X holds

x in Y ) ) implies Z1 = Z2 ) & ( not X <> {} & Z1 = {} & Z2 = {} implies Z1 = Z2 ) )

now :: thesis: ( X <> {} & ( for x being object holds

( x in Z1 iff for Y being set st Y in X holds

x in Y ) ) & ( for x being object holds

( x in Z2 iff for Y being set st Y in X holds

x in Y ) ) implies Z1 = Z2 )

hence
( ( X <> {} & ( for x being object holds ( x in Z1 iff for Y being set st Y in X holds

x in Y ) ) & ( for x being object holds

( x in Z2 iff for Y being set st Y in X holds

x in Y ) ) implies Z1 = Z2 )

assume that

X <> {} and

A4: for x being object holds

( x in Z1 iff for Y being set st Y in X holds

x in Y ) and

A5: for x being object holds

( x in Z2 iff for Y being set st Y in X holds

x in Y ) ; :: thesis: Z1 = Z2

end;X <> {} and

A4: for x being object holds

( x in Z1 iff for Y being set st Y in X holds

x in Y ) and

A5: for x being object holds

( x in Z2 iff for Y being set st Y in X holds

x in Y ) ; :: thesis: Z1 = Z2

now :: thesis: for x being object holds

( x in Z1 iff x in Z2 )

hence
Z1 = Z2
by TARSKI:2; :: thesis: verum( x in Z1 iff x in Z2 )

let x be object ; :: thesis: ( x in Z1 iff x in Z2 )

( x in Z1 iff for Y being set st Y in X holds

x in Y ) by A4;

hence ( x in Z1 iff x in Z2 ) by A5; :: thesis: verum

end;( x in Z1 iff for Y being set st Y in X holds

x in Y ) by A4;

hence ( x in Z1 iff x in Z2 ) by A5; :: thesis: verum

( x in Z1 iff for Y being set st Y in X holds

x in Y ) ) & ( for x being object holds

( x in Z2 iff for Y being set st Y in X holds

x in Y ) ) implies Z1 = Z2 ) & ( not X <> {} & Z1 = {} & Z2 = {} implies Z1 = Z2 ) ) ; :: thesis: verum