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

proof

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

end;

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