theorem Th48: :: EUCLID_7:49

for n being Element of NAT holds RN_Base n is Basis of REAL-US n