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