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 and
A4: [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, A4; :: thesis: verum
end;
assume that
A5: A in D and
A6: B in D and
A7: 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 A8: 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 A5;
consider b being Element of P such that
A9: b in B and
A10: a <= b by A7, A8;
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 A9, A10; :: thesis: verum
end;
hence [A,B] in pcs-general-power-IR (P,D) by A5, A6, Def45; :: thesis: verum