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 Th184; :: thesis: verum