let Z1, Z2 be set ; ( ( 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 ) )
now ( 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 )
;
Z1 = Z2now for x being object holds
( x in Z1 iff x in Z2 )let x be
object ;
( 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;
verum end; hence
Z1 = Z2
by TARSKI:2;
verum end;
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 ) & ( not X <> {} & Z1 = {} & Z2 = {} implies Z1 = Z2 ) )
; verum