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 p', q' being Element of P st p' in p & q' in q holds
p' (--) q'
let D be set ; :: thesis: for p, q being Element of (pcs-general-power P,D) st p (--) q holds
for p', q' being Element of P st p' in p & q' in q holds
p' (--) q'
set R = pcs-general-power P,D;
let p, q be Element of (pcs-general-power P,D); :: thesis: ( p (--) q implies for p', q' being Element of P st p' in p & q' in q holds
p' (--) q' )
assume A1: [p,q] in the ToleranceRel of (pcs-general-power P,D) ; :: according to PCS_0:def 7 :: thesis: for p', q' being Element of P st p' in p & q' in q holds
p' (--) q'
let p', q' be Element of P; :: thesis: ( p' in p & q' in q implies p' (--) q' )
assume ( p' in p & q' in q ) ; :: thesis: p' (--) q'
hence [p',q'] in the ToleranceRel of P by A1, Def46; :: according to PCS_0:def 7 :: thesis: verum