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