A1: 0 in omega ;
A2: omega c= Rank omega by CLASSES1:44;
then reconsider M = Rank omega as non empty set ;
( M is epsilon-transitive & M is Tarski ) by Th70;
then ( M is Universe & M is_Tarski-Class_of {} ) by A1, A2, CLASSES1:def 3;
hence FinSETS c= Rank omega by CLASSES1:def 4; :: according to XBOOLE_0:def 10 :: thesis: Rank omega c= FinSETS
A3: ( On FinSETS <> {} & On FinSETS is limit_ordinal ) by Th55;
then {} in On FinSETS by ORDINAL3:10;
then ( omega c= On FinSETS & FinSETS = Rank (On FinSETS ) ) by A3, Th54, ORDINAL1:def 12;
hence Rank omega c= FinSETS by CLASSES1:43; :: thesis: verum