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 <= q holds
p1 <= q1
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 <= q holds
p1 <= q1
let p, q be Element of P; :: thesis: for p1, q1 being Element of (pcs-extension (P,a)) st p = p1 & q = q1 & p <= q holds
p1 <= q1
let p1, q1 be Element of (pcs-extension (P,a)); :: thesis: ( p = p1 & q = q1 & p <= q implies p1 <= q1 )
assume that
A1: p = p1 and
A2: q = q1 and
A3: [p,q] in the InternalRel of P ; :: according to ORDERS_2:def 5 :: thesis: p1 <= q1
the InternalRel of P c= the InternalRel of (pcs-extension (P,a)) by Th21;
hence [p1,q1] in the InternalRel of (pcs-extension (P,a)) by A1, A2, A3; :: according to ORDERS_2:def 5 :: thesis: verum