let C1, C2, C3 be non empty set ; :: thesis:
let f be RMembership_Func of C1,C2; :: thesis:
let g, h be RMembership_Func of C2,C3; :: thesis:
let x, z be set ; :: thesis:
assume A1: ( x in C1 & z in C3 ) ; :: thesis:
set F = min f,(min g,h),x,z;
set G = min f,g,x,z;
set H = min f,h,x,z;
rng (min f,(min g,h),x,z) is bounded by Th1;
then A2: rng (min f,(min g,h),x,z) is bounded_above by XXREAL_2:def 11;
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;
rng (min f,h,x,z) is bounded by Th1;
then A4: rng (min f,h,x,z) is bounded_above by XXREAL_2:def 11;
A5: for y being set st y in dom (min f,g,x,z) holds
(min f,g,x,z) . y <= sup (rng (min f,g,x,z))

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

end;

A6: for y being set st y in dom (min f,h,x,z) holds
(min f,h,x,z) . y <= sup (rng (min f,h,x,z))

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 <= sup (rng (min f,h,x,z)) by A4, SEQ_4:def 4; :: thesis:

end;

A7: sup (rng (min f,(min g,h),x,z)) <= sup (rng (min f,g,x,z))

A8: for s being real number st 0 < s holds
ex y being set st
( y in dom (min f,(min g,h),x,z) & (sup (rng (min f,(min g,h),x,z))) - s <= (min f,g,x,z) . y )

let s be real number ; :: thesis:
assume 0 < s ; :: thesis:
then consider r being real number such that
A9: ( r in rng (min f,(min g,h),x,z) & (sup (rng (min f,(min g,h),x,z))) - s < r ) by A2, SEQ_4:def 4;
consider y being set such that
A10: ( y in dom (min f,(min g,h),x,z) & r = (min f,(min g,h),x,z) . y ) by A9, FUNCT_1:def 5;
A11: [y,z] in [:C2,C3:] by A1, A10, ZFMISC_1:106;
(min f,(min g,h),x,z) . y = min (f . [x,y]),((min g,h) . [y,z]) by A1, A10, Def2
.= min (f . [x,y]),(min (g . [y,z]),(h . [y,z])) by A11, FUZZY_1:def 4
.= min (min (f . [x,y]),(g . [y,z])),(h . [y,z]) by XXREAL_0:33
.= min ((min f,g,x,z) . y),(h . [y,z]) by A1, A10, Def2 ;
then r <= (min f,g,x,z) . y by A10, XXREAL_0:17;
hence ex y being set st
( y in dom (min f,(min g,h),x,z) & (sup (rng (min f,(min g,h),x,z))) - s <= (min f,g,x,z) . y ) by A9, A10, XXREAL_0:2; :: thesis:

end;

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

let s be real number ; :: thesis:
assume 0 < s ; :: thesis:
then consider y being set such that
A12: ( y in dom (min f,(min g,h),x,z) & (sup (rng (min f,(min g,h),x,z))) - s <= (min f,g,x,z) . y ) by A8;
y in C2 by A12;
then y in dom (min f,g,x,z) by FUNCT_2:def 1;
then (min f,g,x,z) . y <= sup (rng (min f,g,x,z)) by A5;
hence (sup (rng (min f,(min g,h),x,z))) - s <= sup (rng (min f,g,x,z)) by A12, XXREAL_0:2; :: thesis:

end;

hence sup (rng (min f,(min g,h),x,z)) <= sup (rng (min f,g,x,z)) by XREAL_1:59; :: thesis:

end;

sup (rng (min f,(min g,h),x,z)) <= sup (rng (min f,h,x,z))

A13: for s being real number st 0 < s holds
ex y being set st
( y in dom (min f,(min g,h),x,z) & (sup (rng (min f,(min 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
A14: ( r in rng (min f,(min g,h),x,z) & (sup (rng (min f,(min g,h),x,z))) - s < r ) by A2, SEQ_4:def 4;
consider y being set such that
A15: ( y in dom (min f,(min g,h),x,z) & r = (min f,(min g,h),x,z) . y ) by A14, FUNCT_1:def 5;
A16: [y,z] in [:C2,C3:] by A1, A15, ZFMISC_1:106;
(min f,(min g,h),x,z) . y = min (f . [x,y]),((min g,h) . [y,z]) by A1, A15, Def2
.= min (f . [x,y]),(min (g . [y,z]),(h . [y,z])) by A16, FUZZY_1:def 4
.= min (min (f . [x,y]),(h . [y,z])),(g . [y,z]) by XXREAL_0:33
.= min ((min f,h,x,z) . y),(g . [y,z]) by A1, A15, Def2 ;
then r <= (min f,h,x,z) . y by A15, XXREAL_0:17;
hence ex y being set st
( y in dom (min f,(min g,h),x,z) & (sup (rng (min f,(min g,h),x,z))) - s <= (min f,h,x,z) . y ) by A14, A15, XXREAL_0:2; :: thesis:

end;

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

let s be real number ; :: thesis:
assume 0 < s ; :: thesis:
then consider y being set such that
A17: ( y in dom (min f,(min g,h),x,z) & (sup (rng (min f,(min g,h),x,z))) - s <= (min f,h,x,z) . y ) by A13;
y in C2 by A17;
then y in dom (min f,h,x,z) by FUNCT_2:def 1;
then (min f,h,x,z) . y <= sup (rng (min f,h,x,z)) by A6;
hence (sup (rng (min f,(min g,h),x,z))) - s <= sup (rng (min f,h,x,z)) by A17, XXREAL_0:2; :: thesis:

end;

hence sup (rng (min f,(min g,h),x,z)) <= sup (rng (min f,h,x,z)) by XREAL_1:59; :: thesis:

end;

hence sup (rng (min f,(min g,h),x,z)) <= min (sup (rng (min f,g,x,z))),(sup (rng (min f,h,x,z))) by A7, XXREAL_0:20; :: thesis: