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
X c= Y by A1;
hence ( X c= Z & X <> Z ) by A1, A2, XBOOLE_0:def 10; :: according to XBOOLE_0:def 8 :: thesis: verum