theorem :: XBOOLE_1:66

for X being set holds
( X meets X iff X <> {} ) ;