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

assume ( X c= Y & Y c= X & X <> Y ) ; :: according to XBOOLE_0:def 8 :: thesis: contradiction

hence contradiction ; :: thesis: verum