let x be real number ; :: thesis: ( x >= 1 implies (sqrt ((x + 1) / 2)) + (sqrt ((x - 1) / 2)) > 0 )
assume A1: x >= 1 ; :: thesis: (sqrt ((x + 1) / 2)) + (sqrt ((x - 1) / 2)) > 0
then A2: sqrt ((x + 1) / 2) >= 1 by Th8;
(x - 1) / 2 >= 0 by A1, Th7;
then sqrt ((x - 1) / 2) >= 0 by SQUARE_1:82, SQUARE_1:94;
then (sqrt ((x - 1) / 2)) + 1 >= 0 + 1 by XREAL_1:8;
hence (sqrt ((x + 1) / 2)) + (sqrt ((x - 1) / 2)) > 0 by A2, XREAL_1:8; :: thesis: verum