let x be Real; :: 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 (x - 1) / 2 >= 0 by Th7;
then A2: sqrt ((x - 1) / 2) >= 0 by SQUARE_1:17, SQUARE_1:26;
sqrt ((x + 1) / 2) >= 1 by A1, Th8;
hence (sqrt ((x + 1) / 2)) + (sqrt ((x - 1) / 2)) > 0 by A2; :: thesis: verum