let x be RelStr ; :: according to PCS_0:def 4 :: thesis: ( x in rng <%P,Q%> implies x is transitive )
assume x in rng <%P,Q%> ; :: thesis: x is transitive
then x in {P,Q} by Lm3;
hence x is transitive by TARSKI:def 2; :: thesis: verum