theorem :: XBOOLE_0:8

for X, Y being set st X c< Y holds
ex x being object st
( x in Y & X c= Y \ {x} )