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

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

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

end;

given x being object 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 ; :: thesis: verum