let X, Y, Z be set ; :: thesis: ( X c= Y & Y c< Z implies X c< Z )

assume that

A1: X c= Y and

A2: Y c< Z ; :: thesis: X c< Z

Y c= Z by A2;

hence ( X c= Z & X <> Z ) by A1, A2, XBOOLE_0:def 10; :: according to XBOOLE_0:def 8 :: thesis: verum

assume that

A1: X c= Y and

A2: Y c< Z ; :: thesis: X c< Z

Y c= Z by A2;

hence ( X c= Z & X <> Z ) by A1, A2, XBOOLE_0:def 10; :: according to XBOOLE_0:def 8 :: thesis: verum