let n be Element of NAT ; :: thesis: ( 1 <= n implies 1 <= |.(1.REAL n).| )
assume A1: 1 <= n ; :: thesis: 1 <= |.(1.REAL n).|
|.(1.REAL n).| = sqrt n by Th35;
hence 1 <= |.(1.REAL n).| by A1, SQUARE_1:83, SQUARE_1:94; :: thesis: verum