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:87;
(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 4
.= 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 4
.= (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 real-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 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; :: thesis:
assume 0 < s ; :: thesis:
then consider r being Real 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 1;
ex y being object 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 3;
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 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; :: 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 4;
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 3;
rng (min (f,h,x,z)) is real-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 real-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 3;
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 1; :: 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 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:57;
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 3;
rng (max ((min (f,g,x,z)),(min (f,h,x,z)))) is real-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 1; :: thesis:

end;

rng (min (f,h,x,z)) is real-bounded by Th1;
then A22: rng (min (f,h,x,z)) is bounded_above by XXREAL_2:def 11;
A23: for s being Real 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; :: thesis:
assume 0 < s ; :: thesis:
then consider r being Real 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 1;
ex y being object st
( y in dom (min (f,h,x,z)) & r = (min (f,h,x,z)) . y ) by A24, FUNCT_1:def 3;
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 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; :: 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 4;
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:57;
rng (min (f,g,x,z)) is real-bounded by Th1;
then A30: rng (min (f,g,x,z)) is bounded_above by XXREAL_2:def 11;
A31: for s being Real 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; :: thesis:
assume 0 < s ; :: thesis:
then consider r being Real 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 1;
ex y being object st
( y in dom (min (f,g,x,z)) & r = (min (f,g,x,z)) . y ) by A32, FUNCT_1:def 3;
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 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; :: 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 4;
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:57;
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:5; :: thesis: