set f = I --> P;
I --> P is pcs-chain-like

proof

let R, S be pcs-Str ; :: according to PCS_0:def 35 :: thesis: ( R in rng (I --> P) & S in rng (I --> P) & not R c= S implies S c= R )
assume A1: ( R in rng (I --> P) & S in rng (I --> P) ) ; :: thesis: ( R c= S or S c= R )
( ( P = R & P = S ) or rng (I --> P) = {} ) by A1, TARSKI:def 1;
hence ( R c= S or S c= R ) by A1; :: thesis: verum

end;

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