let SFZ, SFX, SFY be set ; ( ( for Z being set holds
( Z in SFZ iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X /\ Y ) ) ) implies for Z being set holds
( Z in SFZ iff ex X, Y being set st
( X in SFY & Y in SFX & Z = X /\ Y ) ) )
assume A14:
for Z being set holds
( Z in SFZ iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X /\ Y ) )
; for Z being set holds
( Z in SFZ iff ex X, Y being set st
( X in SFY & Y in SFX & Z = X /\ Y ) )
let Z be set ; ( Z in SFZ iff ex X, Y being set st
( X in SFY & Y in SFX & Z = X /\ Y ) )
hereby ( ex X, Y being set st
( X in SFY & Y in SFX & Z = X /\ Y ) implies Z in SFZ )
assume
Z in SFZ
;
ex Y, X being set st
( Y in SFY & X in SFX & Z = Y /\ X )then
ex
X,
Y being
set st
(
X in SFX &
Y in SFY &
Z = X /\ Y )
by A14;
hence
ex
Y,
X being
set st
(
Y in SFY &
X in SFX &
Z = Y /\ X )
;
verum
end;
thus
( ex X, Y being set st
( X in SFY & Y in SFX & Z = X /\ Y ) implies Z in SFZ )
by A14; verum