theorem Th72: :: CLASSES4:72

( FinSETS in SETS & NAT in SETS & REAL in SETS & ExtREAL in SETS )