let n be Nat; :: thesis: ( 1 <= n implies 1 <= |.(1.REAL n).| )
assume A1: 1 <= n ; :: thesis: 1 <= |.(1.REAL n).|
|.(1.REAL n).| = sqrt n by Th45;
hence 1 <= |.(1.REAL n).| by A1, SQUARE_1:18, SQUARE_1:26; :: thesis: verum