((b / a) + (a / b)) - 1 >= 2 - 1 by SERIES_3:3, XREAL_1:9;
hence not ((b / a) + (a / b)) - 1 is light ; :: thesis: verum