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

A20: 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

A21: 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

( 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

A20: 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

A21: 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 )

hence
Z1 = Z2
by TARSKI:2; :: thesis: verum( 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 A20;

hence ( Z in Z1 iff Z in Z2 ) by A21; :: thesis: verum

end;( Z in Z1 iff ex X, Y being set st

( X in SFX & Y in SFY & Z = X \ Y ) ) by A20;

hence ( Z in Z1 iff Z in Z2 ) by A21; :: thesis: verum