theorem Th17: :: CLASSES5:17

( union {NAT} c= FinSETS & not union {NAT} in FinSETS & not {NAT} c= FinSETS & not {NAT} in FinSETS )