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

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

assume X meets Y ; :: thesis: ex x being set st
( x in X & x in 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 & x in Y )
thus ( x in X & x in Y ) by A1, Def4; :: thesis: verum

end;

given x being set such that A2: ( x in X & x in Y ) ; :: thesis: X meets Y
x in X /\ Y by A2, Def4;
then X /\ Y <> {} by Def1;
hence X meets Y by Def7; :: thesis: verum