let N be net of T; :: thesis: ( N is constant implies N is convergent )
assume N is constant ; :: thesis: N is convergent
hence Lim N <> {} by Th42; :: according to YELLOW_6:def 19 :: thesis: verum