let P be pcs-Str ; :: thesis: for D being non empty Subset-Family of P
for p, q being Element of (pcs-general-power D) st ( for p9, q9 being Element of P st p9 in p & q9 in q holds
p9 (--) q9 ) holds
p (--) q
let D be non empty Subset-Family of P; :: thesis: for p, q being Element of (pcs-general-power D) st ( for p9, q9 being Element of P st p9 in p & q9 in q holds
p9 (--) q9 ) holds
p (--) q
set R = pcs-general-power D;
let p, q be Element of (pcs-general-power D); :: thesis: ( ( for p9, q9 being Element of P st p9 in p & q9 in q holds
p9 (--) q9 ) implies p (--) q )
assume A1: for p9, q9 being Element of P st p9 in p & q9 in q holds
p9 (--) q9 ; :: thesis: p (--) q
A2: p in D ;
A3: q in D ;
for a, b being set st a in p & b in q holds
[a,b] in the ToleranceRel of P by A1, A2, A3, Def7;
hence [p,q] in the ToleranceRel of (pcs-general-power D) by Def46; :: according to PCS_0:def 7 :: thesis: verum