let P be RelStr ; :: thesis: for D being Subset-Family of P
for A, B being set holds
( [A,B] in pcs-general-power-IR P,D iff ( A in D & B in D & ( for a being Element of P st a in A holds
ex b being Element of P st
( b in B & a <= b ) ) ) )
let D be Subset-Family of P; :: thesis: for A, B being set holds
( [A,B] in pcs-general-power-IR P,D iff ( A in D & B in D & ( for a being Element of P st a in A holds
ex b being Element of P st
( b in B & a <= b ) ) ) )
let A, B be set ; :: thesis: ( [A,B] in pcs-general-power-IR P,D iff ( A in D & B in D & ( for a being Element of P st a in A holds
ex b being Element of P st
( b in B & a <= b ) ) ) )
thus ( [A,B] in pcs-general-power-IR P,D implies ( A in D & B in D & ( for a being Element of P st a in A holds
ex b being Element of P st
( b in B & a <= b ) ) ) ) :: thesis: ( A in D & B in D & ( for a being Element of P st a in A holds
ex b being Element of P st
( b in B & a <= b ) ) implies [A,B] in pcs-general-power-IR P,D )

proof

assume A1: [A,B] in pcs-general-power-IR P,D ; :: thesis: ( A in D & B in D & ( for a being Element of P st a in A holds
ex b being Element of P st
( b in B & a <= b ) ) )
hence A2: ( A in D & B in D ) by Def45; :: thesis: for a being Element of P st a in A holds
ex b being Element of P st
( b in B & a <= b )
let a be Element of P; :: thesis: ( a in A implies ex b being Element of P st
( b in B & a <= b ) )
assume a in A ; :: thesis: ex b being Element of P st
( b in B & a <= b )
then consider b being set such that
A3: ( b in B & [a,b] in the InternalRel of P ) by A1, Def45;
reconsider b = b as Element of P by A2, A3;
take b ; :: thesis: ( b in B & a <= b )
thus ( b in B & a <= b ) by A3, ORDERS_2:def 9; :: thesis: verum

end;

assume that
A4: ( A in D & B in D ) and
A5: for a being Element of P st a in A holds
ex b being Element of P st
( b in B & a <= b ) ; :: thesis: [A,B] in pcs-general-power-IR P,D
for a being set st a in A holds
ex b being set st
( b in B & [a,b] in the InternalRel of P )

proof

let a be set ; :: thesis: ( a in A implies ex b being set st
( b in B & [a,b] in the InternalRel of P ) )
assume A6: a in A ; :: thesis: ex b being set st
( b in B & [a,b] in the InternalRel of P )
then reconsider a = a as Element of P by A4;
consider b being Element of P such that
A7: ( b in B & a <= b ) by A5, A6;
take b ; :: thesis: ( b in B & [a,b] in the InternalRel of P )
thus ( b in B & [a,b] in the InternalRel of P ) by A7, ORDERS_2:def 9; :: thesis: verum

end;

hence [A,B] in pcs-general-power-IR P,D by A4, Def45; :: thesis: verum