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:105;
hence [p,q] in the InternalRel of (pcs-extension (P,a)) by A1, A2, XBOOLE_0:def 3; :: according to ORDERS_2:def 5 :: thesis: verum