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