let r be real number ; :: thesis: [\r/] <= [/r\]
( [\r/] <= r & r <= [/r\] ) by Def4, Def5;
hence [\r/] <= [/r\] by XXREAL_0:2; :: thesis: verum