theorem Th3: :: XBOOLE_0:3

for X, Y being set holds
( X meets Y iff ex x being object st
( x in X & x in Y ) )