let r be real number ; :: thesis: [\r/] <= [/r\]
A1: r <= [/r\] by Def5;
[\r/] <= r by Def6;
hence [\r/] <= [/r\] by A1, XXREAL_0:2; :: thesis: verum