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 that
A1: R in rng (I --> P) and
A2: S in rng (I --> P) ; :: thesis: ( R c= S or S c= R )
( ( P = R & P = S ) or rng (I --> P) = {} ) by A1, A2, TARSKI:def 1;
hence ( R c= S or S c= R ) by A1; :: thesis: verum

end;

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