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:
A3: for y being Element of C2 st y in C2 holds
(min (max f,g),h,x,z) . y = (max (min f,h,x,z),(min g,h,x,z)) . y

let y be Element of C2; :: thesis:
assume y in C2 ; :: thesis:
A4: [x,y] in [:C1,C2:] by A1, ZFMISC_1:106;
(min (max f,g),h,x,z) . y = min ((max f,g) . [x,y]),(h . [y,z]) by A1, A2, Def2
.= min (max (f . [x,y]),(g . [x,y])),(h . [y,z]) by A4, FUZZY_1:def 5
.= max (min (f . [x,y]),(h . [y,z])),(min (g . [x,y]),(h . [y,z])) by XXREAL_0:38
.= max (min (f . [x,y]),(h . [y,z])),((min g,h,x,z) . y) by A1, A2, Def2
.= max ((min f,h,x,z) . y),((min g,h,x,z) . y) by A1, A2, Def2 ;
hence (min (max f,g),h,x,z) . y = (max (min f,h,x,z),(min g,h,x,z)) . y by FUZZY_1:def 5; :: thesis:

end;

set F = min f,h,x,z;
set G = min g,h,x,z;
A5: dom (max (min f,h,x,z),(min g,h,x,z)) = C2 by FUNCT_2:def 1;
rng (max (min f,h,x,z),(min g,h,x,z)) is bounded by Th1;
then A6: rng (max (min f,h,x,z),(min g,h,x,z)) is bounded_above by XXREAL_2:def 11;
A7: for y being set st y in dom (max (min f,h,x,z),(min g,h,x,z)) holds
(max (min f,h,x,z),(min g,h,x,z)) . y <= sup (rng (max (min f,h,x,z),(min g,h,x,z)))

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

end;

rng (min g,h,x,z) is bounded by Th1;
then A8: rng (min g,h,x,z) is bounded_above by XXREAL_2:def 11;
A9: for y being set st y in dom (min g,h,x,z) holds
(min g,h,x,z) . y <= sup (rng (min g,h,x,z))

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

end;

A10: for s being real number st 0 < s holds
ex y being set st
( y in dom (min g,h,x,z) & (sup (rng (min g,h,x,z))) - s <= (max (min f,h,x,z),(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 g,h,x,z) and
A12: (sup (rng (min g,h,x,z))) - s < r by A8, SEQ_4:def 4;
consider y being set such that
A13: y in dom (min g,h,x,z) and
A14: r = (min g,h,x,z) . y by A11, FUNCT_1:def 5;
(min g,h,x,z) . y <= max ((min f,h,x,z) . y),((min g,h,x,z) . y) by XXREAL_0:25;
then r <= (max (min f,h,x,z),(min g,h,x,z)) . y by A13, A14, FUZZY_1:def 5;
hence ex y being set st
( y in dom (min g,h,x,z) & (sup (rng (min g,h,x,z))) - s <= (max (min f,h,x,z),(min g,h,x,z)) . y ) by A12, A13, XXREAL_0:2; :: thesis:

end;

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

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

end;

then A17: sup (rng (min g,h,x,z)) <= sup (rng (max (min f,h,x,z),(min g,h,x,z))) by XREAL_1:59;
rng (min f,h,x,z) is bounded by Th1;
then A18: rng (min f,h,x,z) is bounded_above by XXREAL_2:def 11;
A19: for s being real number st 0 < s holds
ex y being set st
( y in dom (min f,h,x,z) & (sup (rng (min f,h,x,z))) - s <= (max (min f,h,x,z),(min g,h,x,z)) . y )

let s be real number ; :: thesis:
assume 0 < s ; :: thesis:
then consider r being real number such that
A20: r in rng (min f,h,x,z) and
A21: (sup (rng (min f,h,x,z))) - s < r by A18, SEQ_4:def 4;
consider y being set such that
A22: y in dom (min f,h,x,z) and
A23: r = (min f,h,x,z) . y by A20, FUNCT_1:def 5;
(min f,h,x,z) . y <= max ((min f,h,x,z) . y),((min g,h,x,z) . y) by XXREAL_0:25;
then r <= (max (min f,h,x,z),(min g,h,x,z)) . y by A22, A23, FUZZY_1:def 5;
hence ex y being set st
( y in dom (min f,h,x,z) & (sup (rng (min f,h,x,z))) - s <= (max (min f,h,x,z),(min g,h,x,z)) . y ) by A21, A22, XXREAL_0:2; :: thesis:

end;

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

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

end;

then sup (rng (min f,h,x,z)) <= sup (rng (max (min f,h,x,z),(min g,h,x,z))) by XREAL_1:59;
then A26: sup (rng (max (min f,h,x,z),(min g,h,x,z))) >= max (sup (rng (min f,h,x,z))),(sup (rng (min g,h,x,z))) by A17, XXREAL_0:28;
A27: 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 A18, SEQ_4:def 4; :: thesis:

end;

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

let s be real number ; :: thesis:
assume 0 < s ; :: thesis:
then consider r being real number such that
A28: r in rng (max (min f,h,x,z),(min g,h,x,z)) and
A29: (sup (rng (max (min f,h,x,z),(min g,h,x,z)))) - s < r by A6, SEQ_4:def 4;
consider y being set such that
A30: y in dom (max (min f,h,x,z),(min g,h,x,z)) and
A31: r = (max (min f,h,x,z),(min g,h,x,z)) . y by A28, FUNCT_1:def 5;
A32: y in C2 by A30;
then y in dom (min g,h,x,z) by FUNCT_2:def 1;
then A33: (min g,h,x,z) . y <= sup (rng (min g,h,x,z)) by A9;
y in dom (min f,h,x,z) by A32, FUNCT_2:def 1;
then (min f,h,x,z) . y <= sup (rng (min f,h,x,z)) by A27;
then A34: max ((min f,h,x,z) . y),((min g,h,x,z) . y) <= max (sup (rng (min f,h,x,z))),(sup (rng (min g,h,x,z))) by A33, XXREAL_0:26;
(sup (rng (max (min f,h,x,z),(min g,h,x,z)))) - s <= max ((min f,h,x,z) . y),((min g,h,x,z) . y) by A29, A30, A31, FUZZY_1:def 5;
hence (sup (rng (max (min f,h,x,z),(min g,h,x,z)))) - s <= max (sup (rng (min f,h,x,z))),(sup (rng (min g,h,x,z))) by A34, XXREAL_0:2; :: thesis:

end;

then A35: sup (rng (max (min f,h,x,z),(min g,h,x,z))) <= max (sup (rng (min f,h,x,z))),(sup (rng (min g,h,x,z))) by XREAL_1:59;
dom (min (max f,g),h,x,z) = C2 by FUNCT_2:def 1;
then min (max f,g),h,x,z = max (min f,h,x,z),(min g,h,x,z) by A5, A3, PARTFUN1:34;
hence sup (rng (min (max f,g),h,x,z)) = max (sup (rng (min f,h,x,z))),(sup (rng (min g,h,x,z))) by A35, A26, XXREAL_0:1; :: thesis: