let a, b be Real; :: thesis: ( [\a/] <= b & b <= [/a\] & not [\a/] = [\b/] implies [/a\] = [/b\] )
assume A1: ( [\a/] <= b & b <= [/a\] ) ; :: thesis: ( [\a/] = [\b/] or [/a\] = [/b\] )
then A2: ( [\[\a/]/] <= [\b/] & [/b\] <= [/[/a\]\] ) by PRE_FF:9;
A3: ( [/a\] <= [\a/] + 1 & [/b\] <= [\b/] + 1 ) by CF1;

per cases then ( [/b\] = [\b/] + 1 or [/b\] < [\b/] + 1 ) by XXREAL_0:1;

suppose B1: [/b\] = [\b/] + 1 ; :: thesis: ( [\a/] = [\b/] or [/a\] = [/b\] )

( [\a/] + 1 <= [/b\] & [/b\] <= [\a/] + 1 ) by XREAL_1:6, B1, A2, A3, XXREAL_0:2;
then [\a/] + 1 = [/b\] by XXREAL_0:1;
hence ( [\a/] = [\b/] or [/a\] = [/b\] ) by B1; :: thesis: verum

end;

suppose [/b\] < [\b/] + 1 ; :: thesis: ( [\a/] = [\b/] or [/a\] = [/b\] )

then reconsider b = b as Integer by INT_1:41, INT_1:34;
B3: ( [\a/] <= b & b <= [\a/] + 1 ) by A1, A3, XXREAL_0:2;

per cases ( [\a/] = [/a\] or [\a/] + 1 = [/a\] ) by INT_1:41;

suppose [\a/] = [/a\] ; :: thesis: ( [\a/] = [\b/] or [/a\] = [/b\] )

then reconsider a = a as Integer by INT_1:34;
b = a by A1, XXREAL_0:1;
hence ( [\a/] = [\b/] or [/a\] = [/b\] ) ; :: thesis: verum

end;

suppose [\a/] + 1 = [/a\] ; :: thesis: ( [\a/] = [\b/] or [/a\] = [/b\] )

hence ( [\a/] = [\b/] or [/a\] = [/b\] ) by B3, INT17; :: thesis: verum

end;

end;

end;

end;