theorem :: XBOOLE_1:59

for X, Y, Z being set st X c= Y & Y c< Z holds
X c< Z by Lm3;