let C1, C2, C3 be non empty set ; :: thesis:
let f, g be RMembership_Func of C1,C2; :: thesis:
let h be RMembership_Func of C2,C3; :: thesis:
let x, z be set ; :: thesis:
assume that
A1: x in C1 and
A2: z in C3 ; :: thesis:
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 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 number 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 )

let s be real number ; :: thesis:
assume 0 < s ; :: thesis:
then consider r being real number 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 4;
consider y being set 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 5;
A9: [x,y] in [:C1,C2:] by A1, A7, ZFMISC_1:106;
(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 4
.= 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; :: thesis:

end;

A10: for s being real number 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 )

let s be real number ; :: thesis:
assume 0 < s ; :: thesis:
then consider r being real number 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 4;
consider y being set 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 5;
A15: [x,y] in [:C1,C2:] by A1, A13, ZFMISC_1:106;
(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 4
.= 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; :: thesis:

end;

let y be set ; :: thesis:
assume y in dom (min g,h,x,z) ; :: thesis:
then (min g,h,x,z) . y in rng (min g,h,x,z) by FUNCT_1:def 5;
hence (min g,h,x,z) . y <= upper_bound (rng (min g,h,x,z)) by A16, SEQ_4:def 4; :: thesis:

end;

for s being real number st 0 < s holds
(upper_bound (rng (min (min f,g),h,x,z))) - s <= upper_bound (rng (min g,h,x,z))

let s be real number ; :: thesis:
assume 0 < s ; :: thesis:
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; :: thesis:

end;

let y be set ; :: thesis:
assume y in dom (min f,h,x,z) ; :: thesis:
then (min f,h,x,z) . y in rng (min f,h,x,z) by FUNCT_1:def 5;
hence (min f,h,x,z) . y <= upper_bound (rng (min f,h,x,z)) by A21, SEQ_4:def 4; :: thesis:

end;

for s being real number st 0 < s holds
(upper_bound (rng (min (min f,g),h,x,z))) - s <= upper_bound (rng (min f,h,x,z))

let s be real number ; :: thesis:
assume 0 < s ; :: thesis:
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; :: thesis:

end;