let Y be set ; :: thesis: ( ex X being set st
( X <> {} & X in Y ) iff union Y <> {} )
thus ( ex X being set st
( X <> {} & X in Y ) implies union Y <> {} ) :: thesis: ( union Y <> {} implies ex X being set st
( X <> {} & X in Y ) )

proof

given X being set such that A1: X <> {} and
A2: X in Y ; :: thesis: union Y <> {}
set x = the Element of X;
the Element of X in X by A1;
hence union Y <> {} by A2, TARSKI:def 4; :: thesis: verum

end;

set x = the Element of union Y;
assume union Y <> {} ; :: thesis: ex X being set st
( X <> {} & X in Y )
then consider X being set such that
A3: the Element of union Y in X and
A4: X in Y by TARSKI:def 4;
take X ; :: thesis: ( X <> {} & X in Y )
thus ( X <> {} & X in Y ) by A3, A4; :: thesis: verum