let Z1, Z2 be set ; :: thesis: ( ( 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 ) ) ; :: thesis: Z1 = Z2

now :: thesis: for Z being object holds
( Z in Z1 iff Z in Z2 )

let Z be object ; :: thesis: ( 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; :: thesis: verum

end;

hence Z1 = Z2 by TARSKI:2; :: thesis: verum