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 that
A1: x in C1 and
A2: 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 A3: rng (min f,(min 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 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
A5: r in rng (min f,(min g,h),x,z) and
A6: (sup (rng (min f,(min g,h),x,z))) - s < r by A3, SEQ_4:def 4;
consider y being set such that
A7: y in dom (min f,(min g,h),x,z) and
A8: r = (min f,(min g,h),x,z) . y by A5, FUNCT_1:def 5;
A9: [y,z] in [:C2,C3:] by A2, A7, ZFMISC_1:106;
(min f,(min g,h),x,z) . y = min (f . [x,y]),((min g,h) . [y,z]) by A1, A2, A7, Def2
.= min (f . [x,y]),(min (g . [y,z]),(h . [y,z])) by A9, 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, A2, A7, Def2 ;
then r <= (min f,g,x,z) . y by A8, 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 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 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
A11: r in rng (min f,(min g,h),x,z) and
A12: (sup (rng (min f,(min g,h),x,z))) - s < r by A3, SEQ_4:def 4;
consider y being set such that
A13: y in dom (min f,(min g,h),x,z) and
A14: r = (min f,(min g,h),x,z) . y by A11, FUNCT_1:def 5;
A15: [y,z] in [:C2,C3:] by A2, A13, ZFMISC_1:106;
(min f,(min g,h),x,z) . y = min (f . [x,y]),((min g,h) . [y,z]) by A1, A2, A13, Def2
.= min (f . [x,y]),(min (g . [y,z]),(h . [y,z])) by A15, 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, A2, A13, Def2 ;
then r <= (min f,h,x,z) . y by A14, 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 A12, A13, XXREAL_0:2; :: thesis:

end;

rng (min f,h,x,z) is bounded by Th1;
then A16: rng (min f,h,x,z) is bounded_above by XXREAL_2:def 11;
A17: 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 A16, SEQ_4:def 4; :: 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
A18: y in dom (min f,(min g,h),x,z) and
A19: (sup (rng (min f,(min g,h),x,z))) - s <= (min f,h,x,z) . y by A10;
y in C2 by A18;
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 A17;
hence (sup (rng (min f,(min g,h),x,z))) - s <= sup (rng (min f,h,x,z)) by A19, XXREAL_0:2; :: thesis:

end;

then A20: sup (rng (min f,(min g,h),x,z)) <= sup (rng (min f,h,x,z)) by XREAL_1:59;
rng (min f,g,x,z) is bounded by Th1;
then A21: rng (min f,g,x,z) is bounded_above by XXREAL_2:def 11;
A22: 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 A21, SEQ_4:def 4; :: 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
A23: y in dom (min f,(min g,h),x,z) and
A24: (sup (rng (min f,(min g,h),x,z))) - s <= (min f,g,x,z) . y by A4;
y in C2 by A23;
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 A22;
hence (sup (rng (min f,(min g,h),x,z))) - s <= sup (rng (min f,g,x,z)) by A24, XXREAL_0:2; :: thesis:

end;

then sup (rng (min f,(min g,h),x,z)) <= sup (rng (min f,g,x,z)) by XREAL_1:59;
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 A20, XXREAL_0:20; :: thesis: