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 ;

now

let a, b be set ; :: thesis: ( a in p & b in q implies [a,b] in the ToleranceRel of P )
assume that
A4: a in p and
A5: b in q ; :: thesis: [a,b] in the ToleranceRel of P
reconsider a1 = a, b1 = b as Element of P by A2, A3, A4, A5;
a1 (--) b1 by A1, A4, A5;
hence [a,b] in the ToleranceRel of P by Def7; :: thesis: verum

end;

hence [p,q] in the ToleranceRel of (pcs-general-power D) by Def46; :: according to PCS_0:def 7 :: thesis: verum