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, p', q, q' be Element of ; :: according to PCS_0:def 22 :: thesis: ( p (--) q & p' <= p & q' <= q implies p' (--) q' )
assume that
A2: p (--) q and
A3: p' <= p and
A4: q' <= q ; :: thesis: p' (--) q'

per cases ( p' = a or q' = a or ( p' <> a & q' <> a ) ) ;

suppose ( p' = a or q' = a ) ; :: thesis: p' (--) q'

hence p' (--) q' by Th27; :: thesis: verum

end;

suppose that A5: p' <> a and
A6: q' <> a ; :: thesis: p' (--) q'

reconsider p'0 = p', q'0 = q' as Element of by A5, A6, Th25;
A7: p'0 <> a by A5;
A8: q'0 <> 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 by A1, A3, A4, A7, A8, Th24;
A11: p0 (--) q0 by A2, A9, A10, Th29;
A12: p'0 <= p0 by A3, A5, Th26;
q'0 <= q0 by A4, A6, Th26;
then p'0 (--) q'0 by A11, A12, Def22;
hence p' (--) q' by Th28; :: thesis: verum

end;

end;