let P be pcs-Str ; 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 ; 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; 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)); ( 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
; 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;
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:105; ORDERS_2:def 5 verum