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:83, SQUARE_1:95; :: thesis: sqrt x < x
then sqrt x < (sqrt x) ^2 by SQUARE_1:76;
hence sqrt x < x by A1, SQUARE_1:def 4; :: thesis: verum

end;

hereby :: thesis: verum

assume A2: ( 0 < x & x < 1 ) ; :: thesis: ( 0 < sqrt x & sqrt x < 1 & x < sqrt x )
hence A3: 0 < sqrt x by SQUARE_1:82, SQUARE_1:95; :: thesis: ( sqrt x < 1 & x < sqrt x )
thus sqrt x < 1 by A2, SQUARE_1:83, SQUARE_1:95; :: thesis: x < sqrt x
then (sqrt x) ^2 < sqrt x by A3, SQUARE_1:75;
hence x < sqrt x by A2, SQUARE_1:def 4; :: thesis: verum

end;