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