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, XBOOLE_0:def 8;
hence X c< Z by A2, Lm3; :: thesis: verum