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

proof

assume A1: [A,B] in pcs-general-power-TR P,D ; :: thesis: ( A in D & B in D & ( for a, b being Element of P st a in A & b in B holds
a (--) b ) )
hence ( A in D & B in D ) by Def46; :: thesis: for a, b being Element of P st a in A & b in B holds
a (--) b
let a, b be Element of P; :: thesis: ( a in A & b in B implies a (--) b )
assume that
A2: a in A and
A3: b in B ; :: thesis: a (--) b
[a,b] in the ToleranceRel of P by A1, A2, A3, Def46;
hence a (--) b by Def7; :: thesis: verum

end;

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

proof

let a, b be set ; :: thesis: ( a in A & b in B implies [a,b] in the ToleranceRel of P )
assume that
A7: a in A and
A8: b in B ; :: thesis: [a,b] in the ToleranceRel of P
reconsider a = a, b = b as Element of P by A4, A5, A7, A8;
a (--) b by A6, A7, A8;
hence [a,b] in the ToleranceRel of P by Def7; :: thesis: verum

end;

hence [A,B] in pcs-general-power-TR P,D by A4, A5, Def46; :: thesis: verum