let Z1, Z2 be set ; ( ( for Z being set holds
( Z in Z1 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) ) ) & ( for Z being set holds
( Z in Z2 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) ) ) implies Z1 = Z2 )
assume that
A5:
for Z being set holds
( Z in Z1 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) )
and
A6:
for Z being set holds
( Z in Z2 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) )
; Z1 = Z2
now for Z being object holds
( Z in Z1 iff Z in Z2 )let Z be
object ;
( Z in Z1 iff Z in Z2 )
(
Z in Z1 iff ex
X,
Y being
set st
(
X in SFX &
Y in SFY &
Z = X \/ Y ) )
by A5;
hence
(
Z in Z1 iff
Z in Z2 )
by A6;
verum end;
hence
Z1 = Z2
by TARSKI:2; verum