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

proof

let y be Element of C2; :: thesis:
assume y in C2 ; :: thesis:
A4: [x,y] in [:C1,C2:] by A1, ZFMISC_1:87;
(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 4
.= 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 4; :: 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 real-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 <= upper_bound (rng (max ((min (f,h,x,z)),(min (g,h,x,z)))))

proof

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 3;
hence (max ((min (f,h,x,z)),(min (g,h,x,z)))) . y <= upper_bound (rng (max ((min (f,h,x,z)),(min (g,h,x,z))))) by A6, SEQ_4:def 1; :: thesis:

end;

rng (min (g,h,x,z)) is real-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 <= upper_bound (rng (min (g,h,x,z)))

proof

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 3;
hence (min (g,h,x,z)) . y <= upper_bound (rng (min (g,h,x,z))) by A8, SEQ_4:def 1; :: thesis:

end;

A10: for s being Real st 0 < s holds
ex y being set st
( y in dom (min (g,h,x,z)) & (upper_bound (rng (min (g,h,x,z)))) - s <= (max ((min (f,h,x,z)),(min (g,h,x,z)))) . y )

proof

let s be Real; :: thesis:
assume 0 < s ; :: thesis:
then consider r being Real such that
A11: r in rng (min (g,h,x,z)) and
A12: (upper_bound (rng (min (g,h,x,z)))) - s < r by A8, SEQ_4:def 1;
consider y being object 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 3;
(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 4;
hence ex y being set st
( y in dom (min (g,h,x,z)) & (upper_bound (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 st 0 < s holds
(upper_bound (rng (min (g,h,x,z)))) - s <= upper_bound (rng (max ((min (f,h,x,z)),(min (g,h,x,z)))))

proof

let s be Real; :: thesis:
assume 0 < s ; :: thesis:
then consider y being set such that
A15: y in dom (min (g,h,x,z)) and
A16: (upper_bound (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 <= upper_bound (rng (max ((min (f,h,x,z)),(min (g,h,x,z))))) by A7;
hence (upper_bound (rng (min (g,h,x,z)))) - s <= upper_bound (rng (max ((min (f,h,x,z)),(min (g,h,x,z))))) by A16, XXREAL_0:2; :: thesis:

end;

then A17: upper_bound (rng (min (g,h,x,z))) <= upper_bound (rng (max ((min (f,h,x,z)),(min (g,h,x,z))))) by XREAL_1:57;
rng (min (f,h,x,z)) is real-bounded by Th1;
then A18: rng (min (f,h,x,z)) is bounded_above by XXREAL_2:def 11;
A19: 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 <= (max ((min (f,h,x,z)),(min (g,h,x,z)))) . y )

proof

let s be Real; :: thesis:
assume 0 < s ; :: thesis:
then consider r being Real such that
A20: r in rng (min (f,h,x,z)) and
A21: (upper_bound (rng (min (f,h,x,z)))) - s < r by A18, SEQ_4:def 1;
consider y being object 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 3;
(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 4;
hence ex y being set st
( y in dom (min (f,h,x,z)) & (upper_bound (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 st 0 < s holds
(upper_bound (rng (min (f,h,x,z)))) - s <= upper_bound (rng (max ((min (f,h,x,z)),(min (g,h,x,z)))))

proof

let s be Real; :: thesis:
assume 0 < s ; :: thesis:
then consider y being set such that
A24: y in dom (min (f,h,x,z)) and
A25: (upper_bound (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 <= upper_bound (rng (max ((min (f,h,x,z)),(min (g,h,x,z))))) by A7;
hence (upper_bound (rng (min (f,h,x,z)))) - s <= upper_bound (rng (max ((min (f,h,x,z)),(min (g,h,x,z))))) by A25, XXREAL_0:2; :: thesis:

end;

then upper_bound (rng (min (f,h,x,z))) <= upper_bound (rng (max ((min (f,h,x,z)),(min (g,h,x,z))))) by XREAL_1:57;
then A26: upper_bound (rng (max ((min (f,h,x,z)),(min (g,h,x,z))))) >= max ((upper_bound (rng (min (f,h,x,z)))),(upper_bound (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 <= upper_bound (rng (min (f,h,x,z)))

proof

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 3;
hence (min (f,h,x,z)) . y <= upper_bound (rng (min (f,h,x,z))) by A18, SEQ_4:def 1; :: thesis:

end;

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

proof

let s be Real; :: thesis:
assume 0 < s ; :: thesis:
then consider r being Real such that
A28: r in rng (max ((min (f,h,x,z)),(min (g,h,x,z)))) and
A29: (upper_bound (rng (max ((min (f,h,x,z)),(min (g,h,x,z)))))) - s < r by A6, SEQ_4:def 1;
consider y being object 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 3;
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 <= upper_bound (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 <= upper_bound (rng (min (f,h,x,z))) by A27;
then A34: max (((min (f,h,x,z)) . y),((min (g,h,x,z)) . y)) <= max ((upper_bound (rng (min (f,h,x,z)))),(upper_bound (rng (min (g,h,x,z))))) by A33, XXREAL_0:26;
(upper_bound (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 4;
hence (upper_bound (rng (max ((min (f,h,x,z)),(min (g,h,x,z)))))) - s <= max ((upper_bound (rng (min (f,h,x,z)))),(upper_bound (rng (min (g,h,x,z))))) by A34, XXREAL_0:2; :: thesis:

end;

then A35: upper_bound (rng (max ((min (f,h,x,z)),(min (g,h,x,z))))) <= max ((upper_bound (rng (min (f,h,x,z)))),(upper_bound (rng (min (g,h,x,z))))) by XREAL_1:57;
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:5;
hence upper_bound (rng (min ((max (f,g)),h,x,z))) = max ((upper_bound (rng (min (f,h,x,z)))),(upper_bound (rng (min (g,h,x,z))))) by A35, A26, XXREAL_0:1; :: thesis: