let a, b be Element of [.0,1.]; :: thesis: ( a > b implies b / a in [.0,1.] )
assume A0: a > b ; :: thesis: b / a in [.0,1.]
A2: ( 0 <= a & a <= 1 & 0 <= b & b <= 1 ) by XXREAL_1:1;
then b / a <= 1 by XREAL_1:185, A0;
hence b / a in [.0,1.] by A2, XXREAL_1:1; :: thesis: verum