let P be pcs-Str ; :: thesis: for D being non empty Subset-Family of
for p, q being Element of st ( for p' being Element of st p' in p holds
ex q' being Element of st
( q' in q & p' <= q' ) ) holds
p <= q
let D be non empty Subset-Family of ; :: thesis: for p, q being Element of st ( for p' being Element of st p' in p holds
ex q' being Element of st
( q' in q & p' <= q' ) ) holds
p <= q
set R = pcs-general-power D;
let p, q be Element of ; :: thesis: ( ( for p' being Element of st p' in p holds
ex q' being Element of st
( q' in q & p' <= q' ) ) implies p <= q )
assume A1: for p' being Element of st p' in p holds
ex q' being Element of st
( q' in q & p' <= q' ) ; :: thesis: p <= q
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 )

proof

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

end;

hence [p,q] in the InternalRel of (pcs-general-power D) by Def45; :: according to ORDERS_2:def 9 :: thesis: verum