let P be pcs-Str ; :: thesis: for D being set
for p, q being Element of (pcs-general-power P,D) st p <= q holds
for p9 being Element of P st p9 in p holds
ex q9 being Element of P st
( q9 in q & p9 <= q9 )
let D be set ; :: thesis: for p, q being Element of (pcs-general-power P,D) st p <= q holds
for p9 being Element of P st p9 in p holds
ex q9 being Element of P st
( q9 in q & p9 <= q9 )
set R = pcs-general-power P,D;
let p, q be Element of (pcs-general-power P,D); :: thesis: ( p <= q implies for p9 being Element of P st p9 in p holds
ex q9 being Element of P st
( q9 in q & p9 <= q9 ) )
assume A1: [p,q] in the InternalRel of (pcs-general-power P,D) ; :: according to ORDERS_2:def 9 :: thesis: for p9 being Element of P st p9 in p holds
ex q9 being Element of P st
( q9 in q & p9 <= q9 )
let p9 be Element of P; :: thesis: ( p9 in p implies ex q9 being Element of P st
( q9 in q & p9 <= q9 ) )
assume p9 in p ; :: thesis: ex q9 being Element of P st
( q9 in q & p9 <= q9 )
then consider b being set such that
A2: b in q and
A3: [p9,b] in the InternalRel of P by A1, Def45;
reconsider b = b as Element of P by A3, ZFMISC_1:106;
take b ; :: thesis: ( b in q & p9 <= b )
thus ( b in q & [p9,b] in the InternalRel of P ) by A2, A3; :: according to ORDERS_2:def 9 :: thesis: verum