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