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 Th132;
not s in ].r,s.[ by Th4;
hence ].r,s.] \ {s} = ].r,s.[ by A1, ZFMISC_1:141; :: thesis: verum