take {NAT} ; :: thesis: ( union {NAT} is class of FinSETS & {NAT} is not class of FinSETS & {NAT} is not Set of FinSETS & {NAT} is Set of SETS )
( union {NAT} is FinSETS -Class & not {NAT} is FinSETS -Class & not {NAT} is FinSETS -set & {NAT} is SETS -set ) by CLASSES4:72, CLASSES2:57, Th17;
hence ( union {NAT} is class of FinSETS & {NAT} is not class of FinSETS & {NAT} is not Set of FinSETS & {NAT} is Set of SETS ) by Def10, Def12; :: thesis: verum