let a be positive heavy Real; :: thesis: for b being non heavy Real holds
( a > b & b > - a )
let b be non heavy 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