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