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

now :: thesis: for a, b being set st a in p9 & b in q9 holds
[a,b] in the ToleranceRel of P

let a, b be set ; :: thesis: ( a in p9 & b in q9 implies [a,b] in the ToleranceRel of P )
assume that
A8: a in p9 and
A9: b in q9 ; :: thesis: [a,b] in the ToleranceRel of P
reconsider a1 = a, b1 = b as Element of P by A6, A7, A8, A9;
consider p1 being Element of P such that
A10: p1 in p and
A11: a1 <= p1 by A2, A8, Th44;
consider q1 being Element of P 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 ; :: thesis: verum

end;

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