let a be Real; :: thesis: for b being non integer Real st [\a/] <= b & b <= [/a\] holds
( [\a/] = [\b/] & [/a\] = [/b\] )
let b be non integer Real; :: thesis: ( [\a/] <= b & b <= [/a\] implies ( [\a/] = [\b/] & [/a\] = [/b\] ) )
assume A1: ( [\a/] <= b & b <= [/a\] ) ; :: thesis: ( [\a/] = [\b/] & [/a\] = [/b\] )
then reconsider a = a as non integer Real by XXREAL_0:1;
( [\a/] < [/a\] & [\b/] < [/b\] ) by INT_1:35;
then A3: ( [\a/] + 1 = [/a\] & [\b/] + 1 = [/b\] ) by INT_1:41;

per cases ( [\a/] = [\b/] or [/a\] = [/b\] ) by A1, FBC;

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

hence ( [\a/] = [\b/] & [/a\] = [/b\] ) by A3; :: thesis: verum

end;

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

hence ( [\a/] = [\b/] & [/a\] = [/b\] ) by A3; :: thesis: verum

end;

end;