let U be Universe; :: thesis: ( FinSETS c= U & Tarski-Class {} c= U & UNIVERSE {} c= U )
A1: On U c= Rank (On U) by CLASSES1:38;
A2: Rank (On U) = U by Th50;
{} in On U by Th51, ORDINAL3:8;
hence ( FinSETS c= U & Tarski-Class {} c= U & UNIVERSE {} c= U ) by A2, A1, Lm6, Th4; :: thesis: verum