set f = I --> P;
I --> P is pcs-tol-irreflexive-yielding

proof

let S be TolStr ; :: according to PCS_0:def 17 :: thesis: ( S in rng (I --> P) implies S is pcs-tol-irreflexive )
assume S in rng (I --> P) ; :: thesis: S is pcs-tol-irreflexive
hence S is pcs-tol-irreflexive by TARSKI:def 1; :: thesis: verum

end;

hence for b₁ being ManySortedSet of I st b₁ = I --> P holds
b₁ is pcs-tol-irreflexive-yielding ; :: thesis: verum