let i be Integer; :: thesis: for r being Real st 0 < i * r & i * r < r holds
i = 1
let r be Real; :: thesis: ( 0 < i * r & i * r < r implies i = 1 )
assume A1: ( 0 < i * r & i * r < r ) ; :: thesis: i = 1
assume not i = 1 ; :: thesis: contradiction
then ( 0 < 1 - i or 0 < i - 1 ) by XREAL_1:55;
then ( 0 + i < (1 - i) + i or 0 + 1 < (i - 1) + 1 ) by XREAL_1:8;

per cases then ( i < 1 or i > 1 ) ;

suppose i < 1 ; :: thesis: contradiction

then i <= 1 - 1 by INT_1:52;
hence contradiction by A1; :: thesis: verum

end;

suppose i > 1 ; :: thesis: contradiction

hence contradiction by A1, XREAL_1:155; :: thesis: verum

end;

end;