let P be pcs-Str ; :: thesis: for a being set
for p, q being Element of P
for p1, q1 being Element of (pcs-extension P,a) st p = p1 & q = q1 & p <> a & p1 <= q1 holds
p <= q
let a be set ; :: thesis: for p, q being Element of P
for p1, q1 being Element of (pcs-extension P,a) st p = p1 & q = q1 & p <> a & p1 <= q1 holds
p <= q
let p, q be Element of P; :: thesis: for p1, q1 being Element of (pcs-extension P,a) st p = p1 & q = q1 & p <> a & p1 <= q1 holds
p <= q
let p1, q1 be Element of (pcs-extension P,a); :: thesis: ( p = p1 & q = q1 & p <> a & p1 <= q1 implies p <= q )
assume that
A1: p = p1 and
A2: q = q1 and
A3: p <> a and
A4: p1 <= q1 ; :: thesis: p <= q
set R = pcs-extension P,a;
A5: the InternalRel of (pcs-extension P,a) = [:{a},the carrier of (pcs-extension P,a):] \/ the InternalRel of P by Def39;
[p1,q1] in the InternalRel of (pcs-extension P,a) by A4, ORDERS_2:def 9;
then ( [p1,q1] in [:{a},the carrier of (pcs-extension P,a):] or [p1,q1] in the InternalRel of P ) by A5, XBOOLE_0:def 3;
hence [p,q] in the InternalRel of P by A1, A2, A3, ZFMISC_1:128; :: according to ORDERS_2:def 9 :: thesis: verum