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 ) ) ) by Def46; :: 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) )
assume that
A1: A in D and
A2: B in D and
A3: 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 by A1, A2, A3, Def7;
hence [A,B] in pcs-general-power-TR (P,D) by A1, A2, Def46; :: thesis: verum