let X be infinite set ; :: thesis: Tarski-Class {X} c< GrothendieckUniverse {X}
thus Tarski-Class {X} c= GrothendieckUniverse {X} by Th18; :: according to XBOOLE_0:def 8 :: thesis: not Tarski-Class {X} = GrothendieckUniverse {X}
GrothendieckUniverse {X} is union-closed ;
then union {X} in GrothendieckUniverse {X} by Def4;
hence not Tarski-Class {X} = GrothendieckUniverse {X} by Th19; :: thesis: verum