let a, b be Real; :: thesis: ( a <= 1 & 0 <= b & b <= 1 & a * b = 1 implies a = 1 )
assume that
A1: a <= 1 and
A2: 0 <= b and
A3: b <= 1 and
A4: a * b = 1 ; :: thesis: a = 1

now :: thesis: ( ( b = 0 & contradiction ) or ( b > 0 & a = 1 ) )

per cases ( b = 0 or b > 0 ) by A2;

case b = 0 ; :: thesis: contradiction

hence contradiction by A4; :: thesis: verum

end;

case A5: b > 0 ; :: thesis: a = 1

then a = b " by A4, XCMPLX_0:def 7;
then a >= 1 " by A3, A5, Lm32;
hence a = 1 by A1, XXREAL_0:1; :: thesis: verum

end;

end;

end;

hence a = 1 ; :: thesis: verum