( a > 1 implies 1 / a < 1 ) by XREAL_1:189;
hence ( 1 / a is light & 1 / a is positive ) by COMPLEX3:1; :: thesis: verum