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