theorem :: XBOOLE_1:57

for X, Y being set holds
( not X c< Y or not Y c< X ) ;