let r, s be ext-real number ; :: 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