theorem Th17: :: XBOOLE_1:17
for X, Y being set holds X /\ Y c= X by XBOOLE_0:def 4;