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
A4: 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
A5: 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

let Z be set ; :: 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 A4;
hence ( Z in Z1 iff Z in Z2 ) by A5; :: thesis: verum

end;

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