for X, Y being set st X c< Y holds
ex x being object st
( x in Y & not x in X ) by Def8, TARSKI:def 3;