theorem :: CLASSES5:37

( union {NAT} is FinSETS -Class & not {NAT} is FinSETS -Class & not {NAT} is FinSETS -set ) by Th17;