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