let X, Y be set ; :: thesis: ( X meets Y iff ex x being object st x in X /\ Y )

hereby :: thesis: ( ex x being object st x in X /\ Y implies X meets Y )

assume X meets Y ; :: thesis: ex x being object st x in X /\ Y
then X /\ Y <> {} ;
then not X /\ Y is empty by Lm1;
then consider x being object such that
A1: x in X /\ Y ;
take x = x; :: thesis: x in X /\ Y
thus x in X /\ Y by A1; :: thesis: verum

end;

assume ex x being object st x in X /\ Y ; :: thesis: X meets Y
then X /\ Y <> {} by Def1;
hence X meets Y ; :: thesis: verum