theorem Th16: :: CLASSES3:16

for U being Grothendieck
for X being set st X c= U & not X in U holds
ex f being Function st
( f is one-to-one & dom f = On U & rng f = X )