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