let U be Universe; :: thesis: ( FinSETS c= U & Tarski-Class {} c= U & UNIVERSE {} c= U )
{} <> On U by Th55;
then ( {} in On U & Rank (On U) = U & On U c= Rank (On U) ) by Th54, CLASSES1:44, ORDINAL3:10;
hence ( FinSETS c= U & Tarski-Class {} c= U & UNIVERSE {} c= U ) by Lm6, Th5; :: thesis: verum