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