for Y being set holds
( ex X being set st
( X <> {} & X in Y ) iff union Y <> {} ) by Lm1;