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 <> {}
consider x being Element of X;
x in X by A1;
hence union Y <> {} by A2, TARSKI:def 4; :: thesis: verum

end;

consider x being 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: x 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