let X, Y be set ; :: thesis: ( X c= Y implies not Y c< X )
assume ( X c= Y & Y c= X & X <> Y ) ; :: according to XBOOLE_0:def 8 :: thesis: contradiction
hence contradiction ; :: thesis: verum