per cases ( ( a is positive & b is positive ) or ( a is negative & b is negative ) or ( a is positive & b is negative ) or ( a is negative & b is positive ) ) ;
suppose ( a is positive & b is positive ) ; :: thesis: not ((a / b) + (b / a)) / 2 is light
hence not ((a / b) + (b / a)) / 2 is light by PP1, TA1; :: thesis: verum
end;
suppose ( a is negative & b is negative ) ; :: thesis: not ((a / b) + (b / a)) / 2 is light
hence not ((a / b) + (b / a)) / 2 is light by NN1, TA1; :: thesis: verum
end;
suppose ( a is positive & b is negative ) ; :: thesis: not ((a / b) + (b / a)) / 2 is light
hence not ((a / b) + (b / a)) / 2 is light by NP1, TA1; :: thesis: verum
end;
suppose ( a is negative & b is positive ) ; :: thesis: not ((a / b) + (b / a)) / 2 is light
hence not ((a / b) + (b / a)) / 2 is light by NP1, TA1; :: thesis: verum
end;
end;