let X, Y be set ; :: thesis: ( X meets Y implies X /\ Y meets Y )

assume X meets Y ; :: thesis: X /\ Y meets Y

then consider x being object such that

A1: x in X and

A2: x in Y by XBOOLE_0:3;

x in X /\ Y by A1, A2, XBOOLE_0:def 4;

hence X /\ Y meets Y by A2, XBOOLE_0:3; :: thesis: verum

assume X meets Y ; :: thesis: X /\ Y meets Y

then consider x being object such that

A1: x in X and

A2: x in Y by XBOOLE_0:3;

x in X /\ Y by A1, A2, XBOOLE_0:def 4;

hence X /\ Y meets Y by A2, XBOOLE_0:3; :: thesis: verum