let P be pcs-compatible pcs-Str ; :: thesis: for a being set st not a in the carrier of P holds
pcs-extension (P,a) is pcs-compatible
let a be set ; :: thesis: ( not a in the carrier of P implies pcs-extension (P,a) is pcs-compatible )
assume A1: not a in the carrier of P ; :: thesis: pcs-extension (P,a) is pcs-compatible
set R = pcs-extension (P,a);
let p, p9, q, q9 be Element of (pcs-extension (P,a)); :: according to PCS_0:def 22 :: thesis: ( p (--) q & p9 <= p & q9 <= q implies p9 (--) q9 )
assume that
A2: p (--) q and
A3: p9 <= p and
A4: q9 <= q ; :: thesis: p9 (--) q9

per cases ( p9 = a or q9 = a or ( p9 <> a & q9 <> a ) ) ;

suppose ( p9 = a or q9 = a ) ; :: thesis: p9 (--) q9

hence p9 (--) q9 by Th27; :: thesis: verum

end;

suppose that A5: p9 <> a and
A6: q9 <> a ; :: thesis: p9 (--) q9

reconsider p90 = p9, q90 = q9 as Element of P by A5, A6, Th25;
A7: p90 <> a by A5;
A8: q90 <> a by A6;
A9: p <> a by A1, A3, A7, Th24;
A10: q <> a by A1, A4, A8, Th24;
reconsider p0 = p, q0 = q as Element of P by A1, A3, A4, A7, A8, Th24;
A11: p0 (--) q0 by A2, A9, A10, Th29;
A12: p90 <= p0 by A3, A5, Th26;
q90 <= q0 by A4, A6, Th26;
then p90 (--) q90 by A11, A12, Def22;
hence p9 (--) q9 by Th28; :: thesis: verum

end;

end;