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 16 :: thesis: verum