let X be set ; :: thesis: ( X meets X iff X <> {} )

hereby :: thesis: ( X <> {} implies X meets X )

assume X meets X ; :: thesis: X <> {}
then ex x being set st
( x in X & x in X ) by XBOOLE_0:3;
hence X <> {} ; :: thesis: verum

end;

assume X <> {} ; :: thesis: X meets X
then X /\ X <> {} ;
hence X meets X by XBOOLE_0:def 7; :: thesis: verum