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