take f = the carrier of T --> jj; :: thesis: ( f is positive-yielding & f is continuous )

thus f is positive-yielding ; :: thesis: f is continuous

thus f is continuous by Lm1; :: thesis: verum

thus f is positive-yielding ; :: thesis: f is continuous

thus f is continuous by Lm1; :: thesis: verum