let P, Q be TolStr ; :: thesis: for p, q being Element of P
for p1, q1 being Element of Q st the ToleranceRel of P c= the ToleranceRel of Q & p = p1 & q = q1 & p (--) q holds
p1 (--) q1
let p, q be Element of P; :: thesis: for p1, q1 being Element of Q st the ToleranceRel of P c= the ToleranceRel of Q & p = p1 & q = q1 & p (--) q holds
p1 (--) q1
let p1, q1 be Element of Q; :: thesis: ( the ToleranceRel of P c= the ToleranceRel of Q & p = p1 & q = q1 & p (--) q implies p1 (--) q1 )
assume that
A1: the ToleranceRel of P c= the ToleranceRel of Q and
A2: p = p1 and
A3: q = q1 and
A4: [p,q] in the ToleranceRel of P ; :: according to PCS_0:def 7 :: thesis: p1 (--) q1
thus [p1,q1] in the ToleranceRel of Q by A1, A2, A3, A4; :: according to PCS_0:def 7 :: thesis: verum