let P be pcs-Str ; :: thesis:
let D be non empty Subset-Family of P; :: thesis:
set R = pcs-general-power D;
let p, q be Element of (pcs-general-power D); :: thesis:
assume A1: for p9 being Element of P st p9 in p holds
ex q9 being Element of P st
( q9 in q & p9 <= q9 ) ; :: thesis:
A2: p in D ;
for a being set st a in p holds
ex b being set st
( b in q & [a,b] in the InternalRel of P )

let a be set ; :: thesis:
assume A3: a in p ; :: thesis:
then reconsider a = a as Element of P by A2;
consider q9 being Element of P such that
A4: q9 in q and
A5: a <= q9 by A1, A3;
take q9 ; :: thesis:
thus ( q9 in q & [a,q9] in the InternalRel of P ) by A4, A5; :: thesis:

end;