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