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
A10: 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
A11: 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 A10;
hence ( Z in Z1 iff Z in Z2 ) by A11; :: thesis: verum

end;

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