theorem :: EUCLID:75

for n being Nat st 1 <= n holds
1 <= |.(1.REAL n).|