not NAT \/ {NAT} is finite by FINSET_1:13, XBOOLE_1:7;
hence not the carrier of (STC N) is finite by Def11; :: according to STRUCT_0:def 11 :: thesis: verum