let C1, C2, C3 be non empty set ; for f being RMembership_Func of C1,C2
for g being RMembership_Func of C2,C3
for x, z being set st x in C1 & z in C3 holds
upper_bound (rng (min (converse g),(converse f),z,x)) = upper_bound (rng (min f,g,x,z))
let f be RMembership_Func of C1,C2; for g being RMembership_Func of C2,C3
for x, z being set st x in C1 & z in C3 holds
upper_bound (rng (min (converse g),(converse f),z,x)) = upper_bound (rng (min f,g,x,z))
let g be RMembership_Func of C2,C3; for x, z being set st x in C1 & z in C3 holds
upper_bound (rng (min (converse g),(converse f),z,x)) = upper_bound (rng (min f,g,x,z))
let x, z be set ; ( x in C1 & z in C3 implies upper_bound (rng (min (converse g),(converse f),z,x)) = upper_bound (rng (min f,g,x,z)) )
assume that
A1:
x in C1
and
A2:
z in C3
; upper_bound (rng (min (converse g),(converse f),z,x)) = upper_bound (rng (min f,g,x,z))
rng (min f,g,x,z) is bounded
by Th1;
then A3:
rng (min f,g,x,z) is bounded_above
by XXREAL_2:def 11;
for s being real number st 0 < s holds
(upper_bound (rng (min f,g,x,z))) - s <= upper_bound (rng (min (converse g),(converse f),z,x))
proof
let s be
real number ;
( 0 < s implies (upper_bound (rng (min f,g,x,z))) - s <= upper_bound (rng (min (converse g),(converse f),z,x)) )
assume
s > 0
;
(upper_bound (rng (min f,g,x,z))) - s <= upper_bound (rng (min (converse g),(converse f),z,x))
then consider r being
real number such that A4:
r in rng (min f,g,x,z)
and A5:
(upper_bound (rng (min f,g,x,z))) - s < r
by A3, SEQ_4:def 4;
consider y being
set such that A6:
y in dom (min f,g,x,z)
and A7:
r = (min f,g,x,z) . y
by A4, FUNCT_1:def 5;
A8:
[z,y] in [:C3,C2:]
by A2, A6, ZFMISC_1:106;
y in C2
by A6;
then
y in dom (min (converse g),(converse f),z,x)
by FUNCT_2:def 1;
then A9:
(min (converse g),(converse f),z,x) . y <= upper_bound (rng (min (converse g),(converse f),z,x))
by Th1;
A10:
[y,x] in [:C2,C1:]
by A1, A6, ZFMISC_1:106;
r =
min (f . x,y),
(g . y,z)
by A1, A2, A6, A7, Def2
.=
min ((converse f) . y,x),
(g . y,z)
by A10, Def1
.=
min ((converse f) . y,x),
((converse g) . z,y)
by A8, Def1
.=
(min (converse g),(converse f),z,x) . y
by A1, A2, A6, Def2
;
hence
(upper_bound (rng (min f,g,x,z))) - s <= upper_bound (rng (min (converse g),(converse f),z,x))
by A5, A9, XXREAL_0:2;
verum
end;
then A11:
upper_bound (rng (min (converse g),(converse f),z,x)) >= upper_bound (rng (min f,g,x,z))
by XREAL_1:59;
rng (min (converse g),(converse f),z,x) is bounded
by Th1;
then A12:
rng (min (converse g),(converse f),z,x) is bounded_above
by XXREAL_2:def 11;
for s being real number st 0 < s holds
(upper_bound (rng (min (converse g),(converse f),z,x))) - s <= upper_bound (rng (min f,g,x,z))
proof
let s be
real number ;
( 0 < s implies (upper_bound (rng (min (converse g),(converse f),z,x))) - s <= upper_bound (rng (min f,g,x,z)) )
assume
s > 0
;
(upper_bound (rng (min (converse g),(converse f),z,x))) - s <= upper_bound (rng (min f,g,x,z))
then consider r being
real number such that A13:
r in rng (min (converse g),(converse f),z,x)
and A14:
(upper_bound (rng (min (converse g),(converse f),z,x))) - s < r
by A12, SEQ_4:def 4;
consider y being
set such that A15:
y in dom (min (converse g),(converse f),z,x)
and A16:
r = (min (converse g),(converse f),z,x) . y
by A13, FUNCT_1:def 5;
A17:
[z,y] in [:C3,C2:]
by A2, A15, ZFMISC_1:106;
y in C2
by A15;
then
y in dom (min f,g,x,z)
by FUNCT_2:def 1;
then A18:
(min f,g,x,z) . y <= upper_bound (rng (min f,g,x,z))
by Th1;
A19:
[y,x] in [:C2,C1:]
by A1, A15, ZFMISC_1:106;
r =
min ((converse g) . z,y),
((converse f) . y,x)
by A1, A2, A15, A16, Def2
.=
min (g . y,z),
((converse f) . y,x)
by A17, Def1
.=
min (g . y,z),
(f . x,y)
by A19, Def1
.=
(min f,g,x,z) . y
by A1, A2, A15, Def2
;
hence
(upper_bound (rng (min (converse g),(converse f),z,x))) - s <= upper_bound (rng (min f,g,x,z))
by A14, A18, XXREAL_0:2;
verum
end;
then
upper_bound (rng (min (converse g),(converse f),z,x)) <= upper_bound (rng (min f,g,x,z))
by XREAL_1:59;
hence
upper_bound (rng (min (converse g),(converse f),z,x)) = upper_bound (rng (min f,g,x,z))
by A11, XXREAL_0:1; verum