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