set R = pcs-general-power D;
let p, p', q, q' be Element of ; :: according to PCS_0:def 22 :: thesis: ( p (--) q & p' <= p & q' <= q implies p' (--) q' )
assume that
A1: p (--) q and
A2: p' <= p and
A3: q' <= q ; :: thesis: p' (--) q'
A4: [p',p] in the InternalRel of (pcs-general-power D) by A2, ORDERS_2:def 9;
A5: [q',q] in the InternalRel of (pcs-general-power D) by A3, ORDERS_2:def 9;
A6: p' in the carrier of (pcs-general-power D) by A4, ZFMISC_1:106;
A7: q' in the carrier of (pcs-general-power D) by A5, ZFMISC_1:106;

now

let a, b be set ; :: thesis: ( a in p' & b in q' implies [a,b] in the ToleranceRel of P )
assume that
A8: a in p' and
A9: b in q' ; :: thesis: [a,b] in the ToleranceRel of P
reconsider a1 = a, b1 = b as Element of by A6, A7, A8, A9;
consider p1 being Element of such that
A10: p1 in p and
A11: a1 <= p1 by A2, A8, Th44;
consider q1 being Element of such that
A12: q1 in q and
A13: b1 <= q1 by A3, A9, Th44;
p1 (--) q1 by A1, A10, A12, Th46;
then a1 (--) b1 by A11, A13, Def22;
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 A6, Def46; :: according to PCS_0:def 7 :: thesis: verum