theorem :: SUBSET_1:44

for X being non empty set
for A, B being non empty Subset of X st A c< B holds
ex p being Element of X st
( p in B & A c= B \ {p} )