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