for X, Y being set st X c< Y holds
Y \ X <> {} by Th60, Lm1;