let P be RelStr ; 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; 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 ; ( [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 ) ) ) )
( 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) )
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 )
; [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 )
hence
[A,B] in pcs-general-power-IR (P,D)
by A5, A6, Def45; verum