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