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