SETS is_Tarski-Class_of FinSETS by CLASSES1:def 4;
then A1: ( omega c= FinSETS & FinSETS in SETS & SETS is axiom_GU1 & SETS is axiom_GU3 ) by Th16;
then ( NAT in SETS & SETS is Grothendieck ) by Th13;
then reconsider X = SETS as non trivial Universe by Def6;
( REAL is Element of X & ExtREAL is Element of X ) by Th53, Th54;
hence ( FinSETS in SETS & NAT in SETS & REAL in SETS & ExtREAL in SETS ) by A1, Th13; :: thesis: verum