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;