let x be Integer; :: thesis: ( ( 1 < x implies ( 1 < sqrt x & sqrt x < x ) ) & ( 0 < x & x < 1 implies ( 0 < sqrt x & sqrt x < 1 & x < sqrt x ) ) )

hereby :: thesis: ( 0 < x & x < 1 implies ( 0 < sqrt x & sqrt x < 1 & x < sqrt x ) )

assume A1: 1 < x ; :: thesis: ( 1 < sqrt x & sqrt x < x )
hence 1 < sqrt x by SQUARE_1:18, SQUARE_1:27; :: thesis: sqrt x < x
then sqrt x < (sqrt x) ^2 by SQUARE_1:14;
hence sqrt x < x by A1, SQUARE_1:def 2; :: thesis: verum

end;

hereby :: thesis: verum

assume that
A2: 0 < x and
A3: x < 1 ; :: thesis: ( 0 < sqrt x & sqrt x < 1 & x < sqrt x )
thus A4: 0 < sqrt x by A2, SQUARE_1:17, SQUARE_1:27; :: thesis: ( sqrt x < 1 & x < sqrt x )
thus sqrt x < 1 by A2, A3, SQUARE_1:18, SQUARE_1:27; :: thesis: x < sqrt x
then (sqrt x) ^2 < sqrt x by A4, SQUARE_1:13;
hence x < sqrt x by A2, SQUARE_1:def 2; :: thesis: verum

end;