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