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