set R = pcs-general-power D;
let p, p9, q, q9 be Element of (pcs-general-power D); PCS_0:def 22 ( p (--) q & p9 <= p & q9 <= q implies p9 (--) q9 )
assume that
A1:
p (--) q
and
A2:
p9 <= p
and
A3:
q9 <= q
; 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 for a, b being set st a in p9 & b in q9 holds
[a,b] in the ToleranceRel of Plet a,
b be
set ;
( 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
;
[a,b] in the ToleranceRel of Preconsider 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
;
verum end;
hence
[p9,q9] in the ToleranceRel of (pcs-general-power D)
by A6, Def46; PCS_0:def 7 verum