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

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

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

end;

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