let a, b be positive Real; :: thesis: ( a - b = a * b implies b is light )
( not b is light implies (1 / b) - (1 / a) < 1 )

proof

assume not b is light ; :: thesis: (1 / b) - (1 / a) < 1
then 1 / b <= 1 by TA1;
then A1: (1 / b) - (1 / a) <= 1 - (1 / a) by XREAL_1:9;
1 - (1 / a) < 1 - 0 by XREAL_1:15;
hence (1 / b) - (1 / a) < 1 by A1, XXREAL_0:2; :: thesis: verum

end;

hence ( a - b = a * b implies b is light ) by DIO; :: thesis: verum