let P be pcs-compatible pcs-Str ; for a being set st not a in the carrier of P holds
pcs-extension (P,a) is pcs-compatible
let a be set ; ( not a in the carrier of P implies pcs-extension (P,a) is pcs-compatible )
assume A1:
not a in the carrier of P
; 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)); PCS_0:def 22 ( p (--) q & p9 <= p & q9 <= q implies p9 (--) q9 )
assume that
A2:
p (--) q
and
A3:
p9 <= p
and
A4:
q9 <= q
; p9 (--) q9
per cases
( p9 = a or q9 = a or ( p9 <> a & q9 <> a ) )
;
suppose that A5:
p9 <> a
and A6:
q9 <> a
;
p9 (--) q9reconsider 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;
verum end;