let a, b be real number ; :: thesis: ( 0 <= a & a <= 1 & 0 <= b & b <= 1 & a * b = 1 implies a = 1 )
assume A1: ( 0 <= a & a <= 1 & 0 <= b & b <= 1 & a * b = 1 ) ; :: thesis: a = 1

now

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

case b = 0 ; :: thesis: contradiction

hence contradiction by A1; :: thesis: verum

end;

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

then a = b " by A1, XCMPLX_0:def 7;
then a >= 1 " by A1, A2, Lm36;
hence a = 1 by A1, XXREAL_0:1; :: thesis: verum

end;

end;

end;

hence a = 1 ; :: thesis: verum