theorem Th60: :: XBOOLE_1:60

for X, Y being set st X c= Y holds
not Y c< X