let P be pcs-Str ; :: thesis: for a being set
for p being Element of P
for p1, q1 being Element of (pcs-extension (P,a)) st p = p1 & p <> a & p1 <= q1 & not a in the carrier of P holds
( q1 in the carrier of P & q1 <> a )
let a be set ; :: thesis: for p being Element of P
for p1, q1 being Element of (pcs-extension (P,a)) st p = p1 & p <> a & p1 <= q1 & not a in the carrier of P holds
( q1 in the carrier of P & q1 <> a )
let p be Element of P; :: thesis: for p1, q1 being Element of (pcs-extension (P,a)) st p = p1 & p <> a & p1 <= q1 & not a in the carrier of P holds
( q1 in the carrier of P & q1 <> a )
let p1, q1 be Element of (pcs-extension (P,a)); :: thesis: ( p = p1 & p <> a & p1 <= q1 & not a in the carrier of P implies ( q1 in the carrier of P & q1 <> a ) )
assume that
A1: p = p1 and
A2: p <> a and
A3: p1 <= q1 and
A4: not a in the carrier of P ; :: thesis: ( q1 in the carrier of P & q1 <> a )
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 A3;
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 ( q1 in the carrier of P & q1 <> a ) by A1, A2, A4, ZFMISC_1:87, ZFMISC_1:105; :: thesis: verum