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 Th17, CLASSES2:57, CLASSES4:72;
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