let x, y be Element of [.0,1.]; :: thesis: ( x <> 0 implies y <= y / x )
assume x <> 0 ; :: thesis: y <= y / x
then ( x <= 1 & y >= 0 & x > 0 ) by XXREAL_1:1;
then y / 1 <= y / x by XREAL_1:118;
hence y <= y / x ; :: thesis: verum