A1: omega c= FinSETS by Th16;

now :: thesis: ( omega = FinSETS implies omega c< FinSETS )

assume A2: omega = FinSETS ; :: thesis: omega c< FinSETS
then reconsider x1 = 1 as Element of FinSETS ;
{x1} in FinSETS ;
then A3: {1} is epsilon-transitive by A2;
A4: 1 in {1} by TARSKI:def 1;
not 1 c= {1}

proof

assume A5: 1 c= {1} ; :: thesis: contradiction
0 in 1 by CARD_1:49, TARSKI:def 1;
hence contradiction by A5; :: thesis: verum

end;

hence omega c< FinSETS by A4, A3; :: thesis: verum

end;

hence omega c< FinSETS by A1; :: thesis: verum