theorem :: CLASSES3:20

for X being infinite set holds Tarski-Class {X} c< GrothendieckUniverse {X}