let a be positive non light Real; :: thesis: for b being light Real holds
( a > b & b > - a )
let b be light Real; :: thesis: ( a > b & b > - a )
( a >= 1 & 1 > b & b > - 1 & - 1 >= - a ) by TA1;
hence ( a > b & b > - a ) by XXREAL_0:2; :: thesis: verum