let r, s be ext-real number ; :: thesis: ( r <= s implies [.r,s.] \ {r} = ].r,s.] )
assume r <= s ; :: thesis: [.r,s.] \ {r} = ].r,s.]
then A1: [.r,s.] = {r} \/ ].r,s.] by Th130;
not r in ].r,s.] by Th2;
hence [.r,s.] \ {r} = ].r,s.] by A1, ZFMISC_1:141; :: thesis: verum