let C1, C2, C3 be non empty set ; for f, g being RMembership_Func of C1,C2
for h being RMembership_Func of C2,C3
for x, z being set st x in C1 & z in C3 holds
upper_bound (rng (min ((min (f,g)),h,x,z))) <= min ((upper_bound (rng (min (f,h,x,z)))),(upper_bound (rng (min (g,h,x,z)))))
let f, g be RMembership_Func of C1,C2; for h being RMembership_Func of C2,C3
for x, z being set st x in C1 & z in C3 holds
upper_bound (rng (min ((min (f,g)),h,x,z))) <= min ((upper_bound (rng (min (f,h,x,z)))),(upper_bound (rng (min (g,h,x,z)))))
let h be RMembership_Func of C2,C3; for x, z being set st x in C1 & z in C3 holds
upper_bound (rng (min ((min (f,g)),h,x,z))) <= min ((upper_bound (rng (min (f,h,x,z)))),(upper_bound (rng (min (g,h,x,z)))))
let x, z be set ; ( x in C1 & z in C3 implies upper_bound (rng (min ((min (f,g)),h,x,z))) <= min ((upper_bound (rng (min (f,h,x,z)))),(upper_bound (rng (min (g,h,x,z))))) )
assume that
A1:
x in C1
and
A2:
z in C3
; upper_bound (rng (min ((min (f,g)),h,x,z))) <= min ((upper_bound (rng (min (f,h,x,z)))),(upper_bound (rng (min (g,h,x,z)))))
set F = min ((min (f,g)),h,x,z);
set G = min (f,h,x,z);
set H = min (g,h,x,z);
rng (min ((min (f,g)),h,x,z)) is real-bounded
by Th1;
then A3:
rng (min ((min (f,g)),h,x,z)) is bounded_above
by XXREAL_2:def 11;
A4:
for s being Real st 0 < s holds
ex y being set st
( y in dom (min ((min (f,g)),h,x,z)) & (upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= (min (f,h,x,z)) . y )
proof
let s be
Real;
( 0 < s implies ex y being set st
( y in dom (min ((min (f,g)),h,x,z)) & (upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= (min (f,h,x,z)) . y ) )
assume
0 < s
;
ex y being set st
( y in dom (min ((min (f,g)),h,x,z)) & (upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= (min (f,h,x,z)) . y )
then consider r being
Real such that A5:
r in rng (min ((min (f,g)),h,x,z))
and A6:
(upper_bound (rng (min ((min (f,g)),h,x,z)))) - s < r
by A3, SEQ_4:def 1;
consider y being
object such that A7:
y in dom (min ((min (f,g)),h,x,z))
and A8:
r = (min ((min (f,g)),h,x,z)) . y
by A5, FUNCT_1:def 3;
A9:
[x,y] in [:C1,C2:]
by A1, A7, ZFMISC_1:87;
(min ((min (f,g)),h,x,z)) . y =
min (
((min (f,g)) . [x,y]),
(h . [y,z]))
by A1, A2, A7, Def2
.=
min (
(min ((f . [x,y]),(g . [x,y]))),
(h . [y,z]))
by A9, FUZZY_1:def 3
.=
min (
(min ((h . [y,z]),(f . [x,y]))),
(g . [x,y]))
by XXREAL_0:33
.=
min (
((min (f,h,x,z)) . y),
(g . [x,y]))
by A1, A2, A7, Def2
;
then
r <= (min (f,h,x,z)) . y
by A8, XXREAL_0:17;
hence
ex
y being
set st
(
y in dom (min ((min (f,g)),h,x,z)) &
(upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= (min (f,h,x,z)) . y )
by A6, A7, XXREAL_0:2;
verum
end;
A10:
for s being Real st 0 < s holds
ex y being set st
( y in dom (min ((min (f,g)),h,x,z)) & (upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= (min (g,h,x,z)) . y )
proof
let s be
Real;
( 0 < s implies ex y being set st
( y in dom (min ((min (f,g)),h,x,z)) & (upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= (min (g,h,x,z)) . y ) )
assume
0 < s
;
ex y being set st
( y in dom (min ((min (f,g)),h,x,z)) & (upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= (min (g,h,x,z)) . y )
then consider r being
Real such that A11:
r in rng (min ((min (f,g)),h,x,z))
and A12:
(upper_bound (rng (min ((min (f,g)),h,x,z)))) - s < r
by A3, SEQ_4:def 1;
consider y being
object such that A13:
y in dom (min ((min (f,g)),h,x,z))
and A14:
r = (min ((min (f,g)),h,x,z)) . y
by A11, FUNCT_1:def 3;
A15:
[x,y] in [:C1,C2:]
by A1, A13, ZFMISC_1:87;
(min ((min (f,g)),h,x,z)) . y =
min (
((min (f,g)) . [x,y]),
(h . [y,z]))
by A1, A2, A13, Def2
.=
min (
(min ((f . [x,y]),(g . [x,y]))),
(h . [y,z]))
by A15, FUZZY_1:def 3
.=
min (
(f . [x,y]),
(min ((h . [y,z]),(g . [x,y]))))
by XXREAL_0:33
.=
min (
((min (g,h,x,z)) . y),
(f . [x,y]))
by A1, A2, A13, Def2
;
then
r <= (min (g,h,x,z)) . y
by A14, XXREAL_0:17;
hence
ex
y being
set st
(
y in dom (min ((min (f,g)),h,x,z)) &
(upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= (min (g,h,x,z)) . y )
by A12, A13, XXREAL_0:2;
verum
end;
rng (min (g,h,x,z)) is real-bounded
by Th1;
then A16:
rng (min (g,h,x,z)) is bounded_above
by XXREAL_2:def 11;
A17:
for y being set st y in dom (min (g,h,x,z)) holds
(min (g,h,x,z)) . y <= upper_bound (rng (min (g,h,x,z)))
proof
let y be
set ;
( y in dom (min (g,h,x,z)) implies (min (g,h,x,z)) . y <= upper_bound (rng (min (g,h,x,z))) )
assume
y in dom (min (g,h,x,z))
;
(min (g,h,x,z)) . y <= upper_bound (rng (min (g,h,x,z)))
then
(min (g,h,x,z)) . y in rng (min (g,h,x,z))
by FUNCT_1:def 3;
hence
(min (g,h,x,z)) . y <= upper_bound (rng (min (g,h,x,z)))
by A16, SEQ_4:def 1;
verum
end;
for s being Real st 0 < s holds
(upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= upper_bound (rng (min (g,h,x,z)))
proof
let s be
Real;
( 0 < s implies (upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= upper_bound (rng (min (g,h,x,z))) )
assume
0 < s
;
(upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= upper_bound (rng (min (g,h,x,z)))
then consider y being
set such that A18:
y in dom (min ((min (f,g)),h,x,z))
and A19:
(upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= (min (g,h,x,z)) . y
by A10;
y in C2
by A18;
then
y in dom (min (g,h,x,z))
by FUNCT_2:def 1;
then
(min (g,h,x,z)) . y <= upper_bound (rng (min (g,h,x,z)))
by A17;
hence
(upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= upper_bound (rng (min (g,h,x,z)))
by A19, XXREAL_0:2;
verum
end;
then A20:
upper_bound (rng (min ((min (f,g)),h,x,z))) <= upper_bound (rng (min (g,h,x,z)))
by XREAL_1:57;
rng (min (f,h,x,z)) is real-bounded
by Th1;
then A21:
rng (min (f,h,x,z)) is bounded_above
by XXREAL_2:def 11;
A22:
for y being set st y in dom (min (f,h,x,z)) holds
(min (f,h,x,z)) . y <= upper_bound (rng (min (f,h,x,z)))
proof
let y be
set ;
( y in dom (min (f,h,x,z)) implies (min (f,h,x,z)) . y <= upper_bound (rng (min (f,h,x,z))) )
assume
y in dom (min (f,h,x,z))
;
(min (f,h,x,z)) . y <= upper_bound (rng (min (f,h,x,z)))
then
(min (f,h,x,z)) . y in rng (min (f,h,x,z))
by FUNCT_1:def 3;
hence
(min (f,h,x,z)) . y <= upper_bound (rng (min (f,h,x,z)))
by A21, SEQ_4:def 1;
verum
end;
for s being Real st 0 < s holds
(upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= upper_bound (rng (min (f,h,x,z)))
proof
let s be
Real;
( 0 < s implies (upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= upper_bound (rng (min (f,h,x,z))) )
assume
0 < s
;
(upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= upper_bound (rng (min (f,h,x,z)))
then consider y being
set such that A23:
y in dom (min ((min (f,g)),h,x,z))
and A24:
(upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= (min (f,h,x,z)) . y
by A4;
y in C2
by A23;
then
y in dom (min (f,h,x,z))
by FUNCT_2:def 1;
then
(min (f,h,x,z)) . y <= upper_bound (rng (min (f,h,x,z)))
by A22;
hence
(upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= upper_bound (rng (min (f,h,x,z)))
by A24, XXREAL_0:2;
verum
end;
then
upper_bound (rng (min ((min (f,g)),h,x,z))) <= upper_bound (rng (min (f,h,x,z)))
by XREAL_1:57;
hence
upper_bound (rng (min ((min (f,g)),h,x,z))) <= min ((upper_bound (rng (min (f,h,x,z)))),(upper_bound (rng (min (g,h,x,z)))))
by A20, XXREAL_0:20; verum