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