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

proof

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

end;

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

proof

let s be real number ; :: thesis:
assume 0 < s ; :: thesis:
then consider r being real number such that
A8: r in rng (max (min f,g,x,z),(min f,h,x,z)) and
A9: (upper_bound (rng (max (min f,g,x,z),(min f,h,x,z)))) - s < r by A6, SEQ_4:def 4;
ex y being set st
( y in dom (max (min f,g,x,z),(min f,h,x,z)) & r = (max (min f,g,x,z),(min f,h,x,z)) . y ) by A8, FUNCT_1:def 5;
hence ex y being set st
( y in dom (max (min f,g,x,z),(min f,h,x,z)) & (upper_bound (rng (max (min f,g,x,z),(min f,h,x,z)))) - s < (max (min f,g,x,z),(min f,h,x,z)) . y ) by A9; :: thesis:

end;

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

proof

let s be real number ; :: thesis:
assume 0 < s ; :: thesis:
then consider y being set such that
A10: y in dom (max (min f,g,x,z),(min f,h,x,z)) and
A11: (upper_bound (rng (max (min f,g,x,z),(min f,h,x,z)))) - s < (max (min f,g,x,z),(min f,h,x,z)) . y by A7;
A12: (max (min f,g,x,z),(min f,h,x,z)) . y = max ((min f,g,x,z) . y),((min f,h,x,z) . y) by A10, FUZZY_1:def 5;
A13: for y being set st y in C2 holds
( (min f,g,x,z) . y <= upper_bound (rng (min f,g,x,z)) & (min f,h,x,z) . y <= upper_bound (rng (min f,h,x,z)) )

proof

let y be set ; :: thesis:
assume A14: y in C2 ; :: thesis:
then y in dom (min f,h,x,z) by FUNCT_2:def 1;
then A15: (min f,h,x,z) . y in rng (min f,h,x,z) by FUNCT_1:def 5;
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;
rng (min f,g,x,z) is bounded by Th1;
then A17: rng (min f,g,x,z) is bounded_above by XXREAL_2:def 11;
y in dom (min f,g,x,z) by A14, FUNCT_2:def 1;
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 <= upper_bound (rng (min f,g,x,z)) & (min f,h,x,z) . y <= upper_bound (rng (min f,h,x,z)) ) by A15, A17, A16, SEQ_4:def 4; :: thesis:

end;

then A18: (min f,h,x,z) . y <= upper_bound (rng (min f,h,x,z)) by A10;
(min f,g,x,z) . y <= upper_bound (rng (min f,g,x,z)) by A10, A13;
then (max (min f,g,x,z),(min f,h,x,z)) . y <= max (upper_bound (rng (min f,g,x,z))),(upper_bound (rng (min f,h,x,z))) by A12, A18, XXREAL_0:26;
hence (upper_bound (rng (max (min f,g,x,z),(min f,h,x,z)))) - s < max (upper_bound (rng (min f,g,x,z))),(upper_bound (rng (min f,h,x,z))) by A11, XXREAL_0:2; :: thesis:

end;

then for s being real number st 0 < s holds
(upper_bound (rng (max (min f,g,x,z),(min f,h,x,z)))) - s <= max (upper_bound (rng (min f,g,x,z))),(upper_bound (rng (min f,h,x,z))) ;
then A19: upper_bound (rng (max (min f,g,x,z),(min f,h,x,z))) <= max (upper_bound (rng (min f,g,x,z))),(upper_bound (rng (min f,h,x,z))) by XREAL_1:59;
A20: for y being set st y in C2 holds
(max (min f,g,x,z),(min f,h,x,z)) . y <= upper_bound (rng (max (min f,g,x,z),(min f,h,x,z)))

proof

let y be set ; :: thesis:
assume y in C2 ; :: thesis:
then y in dom (max (min f,g,x,z),(min f,h,x,z)) by FUNCT_2:def 1;
then A21: (max (min f,g,x,z),(min f,h,x,z)) . y in rng (max (min f,g,x,z),(min f,h,x,z)) by FUNCT_1:def 5;
rng (max (min f,g,x,z),(min f,h,x,z)) is bounded by Th1;
then rng (max (min f,g,x,z),(min f,h,x,z)) is bounded_above by XXREAL_2:def 11;
hence (max (min f,g,x,z),(min f,h,x,z)) . y <= upper_bound (rng (max (min f,g,x,z),(min f,h,x,z))) by A21, SEQ_4:def 4; :: thesis:

end;

rng (min f,h,x,z) is bounded by Th1;
then A22: rng (min f,h,x,z) is bounded_above by XXREAL_2:def 11;
A23: for s being real number st 0 < s holds
ex y being set st
( y in dom (min f,h,x,z) & (upper_bound (rng (min f,h,x,z))) - s < (min f,h,x,z) . y )

proof

let s be real number ; :: thesis:
assume 0 < s ; :: thesis:
then consider r being real number such that
A24: r in rng (min f,h,x,z) and
A25: (upper_bound (rng (min f,h,x,z))) - s < r by A22, SEQ_4:def 4;
ex y being set st
( y in dom (min f,h,x,z) & r = (min f,h,x,z) . y ) by A24, FUNCT_1:def 5;
hence ex y being set st
( y in dom (min f,h,x,z) & (upper_bound (rng (min f,h,x,z))) - s < (min f,h,x,z) . y ) by A25; :: thesis:

end;

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

proof

let s be real number ; :: thesis:
assume 0 < s ; :: thesis:
then consider y being set such that
A26: y in dom (min f,h,x,z) and
A27: (upper_bound (rng (min f,h,x,z))) - s < (min f,h,x,z) . y by A23;
(min f,h,x,z) . y <= max ((min f,g,x,z) . y),((min f,h,x,z) . y) by XXREAL_0:25;
then (min f,h,x,z) . y <= (max (min f,g,x,z),(min f,h,x,z)) . y by A26, FUZZY_1:def 5;
then A28: (upper_bound (rng (min f,h,x,z))) - s < (max (min f,g,x,z),(min f,h,x,z)) . y by A27, XXREAL_0:2;
(max (min f,g,x,z),(min f,h,x,z)) . y <= upper_bound (rng (max (min f,g,x,z),(min f,h,x,z))) by A20, A26;
hence (upper_bound (rng (min f,h,x,z))) - s <= upper_bound (rng (max (min f,g,x,z),(min f,h,x,z))) by A28, XXREAL_0:2; :: thesis:

end;

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

proof

let s be real number ; :: thesis:
assume 0 < s ; :: thesis:
then consider r being real number such that
A32: r in rng (min f,g,x,z) and
A33: (upper_bound (rng (min f,g,x,z))) - s < r by A30, SEQ_4:def 4;
ex y being set st
( y in dom (min f,g,x,z) & r = (min f,g,x,z) . y ) by A32, FUNCT_1:def 5;
hence ex y being set st
( y in dom (min f,g,x,z) & (upper_bound (rng (min f,g,x,z))) - s < (min f,g,x,z) . y ) by A33; :: thesis:

end;

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

proof

let s be real number ; :: thesis:
assume 0 < s ; :: thesis:
then consider y being set such that
A34: y in dom (min f,g,x,z) and
A35: (upper_bound (rng (min f,g,x,z))) - s < (min f,g,x,z) . y by A31;
(min f,g,x,z) . y <= max ((min f,g,x,z) . y),((min f,h,x,z) . y) by XXREAL_0:25;
then (min f,g,x,z) . y <= (max (min f,g,x,z),(min f,h,x,z)) . y by A34, FUZZY_1:def 5;
then A36: (upper_bound (rng (min f,g,x,z))) - s < (max (min f,g,x,z),(min f,h,x,z)) . y by A35, XXREAL_0:2;
(max (min f,g,x,z),(min f,h,x,z)) . y <= upper_bound (rng (max (min f,g,x,z),(min f,h,x,z))) by A20, A34;
hence (upper_bound (rng (min f,g,x,z))) - s <= upper_bound (rng (max (min f,g,x,z),(min f,h,x,z))) by A36, XXREAL_0:2; :: thesis:

end;

then upper_bound (rng (min f,g,x,z)) <= upper_bound (rng (max (min f,g,x,z),(min f,h,x,z))) by XREAL_1:59;
then max (upper_bound (rng (min f,g,x,z))),(upper_bound (rng (min f,h,x,z))) <= upper_bound (rng (max (min f,g,x,z),(min f,h,x,z))) by A29, XXREAL_0:28;
then A37: upper_bound (rng (max (min f,g,x,z),(min f,h,x,z))) = max (upper_bound (rng (min f,g,x,z))),(upper_bound (rng (min f,h,x,z))) by A19, XXREAL_0:1;
dom (max (min f,g,x,z),(min f,h,x,z)) = C2 by FUNCT_2:def 1;
hence upper_bound (rng (min f,(max g,h),x,z)) = max (upper_bound (rng (min f,g,x,z))),(upper_bound (rng (min f,h,x,z))) by A5, A3, A37, PARTFUN1:34; :: thesis: