SETS is_Tarski-Class_of FinSETS by CLASSES1:def 4;
then ( omega c= FinSETS & FinSETS in SETS & SETS is axiom_GU1 & SETS is axiom_GU3 ) by Th16;
hence ( FinSETS is trivial & not SETS is trivial ) by Th13, Th19, Th20; :: thesis: verum