consider R being non empty transitive directed RelStr , p being Point of T;
take ConstantNet (R,p) ; :: thesis: ( ConstantNet (R,p) is convergent & ConstantNet (R,p) is strict )
thus ( ConstantNet (R,p) is convergent & ConstantNet (R,p) is strict ) ; :: thesis: verum