let r, s be ExtReal; :: thesis: ( r < s implies ].r,s.] \ ].r,s.[ = {s} )
[.s,s.] = {s} by Th17;
hence ( r < s implies ].r,s.] \ ].r,s.[ = {s} ) by Th188; :: thesis: verum