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:
set F = min ((min (f,g)),h,x,z);
set G = min (f,h,x,z);
set H = min (g,h,x,z);
rng (min ((min (f,g)),h,x,z)) is real-bounded by Th1;
then A3: rng (min ((min (f,g)),h,x,z)) is bounded_above by XXREAL_2:def 11;
A4: for s being Real st 0 < s holds
ex y being set st
( y in dom (min ((min (f,g)),h,x,z)) & (upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= (min (f,h,x,z)) . y )

let s be Real; :: thesis:
assume 0 < s ; :: thesis:
then consider r being Real such that
A5: r in rng (min ((min (f,g)),h,x,z)) and
A6: (upper_bound (rng (min ((min (f,g)),h,x,z)))) - s < r by A3, SEQ_4:def 1;
consider y being object such that
A7: y in dom (min ((min (f,g)),h,x,z)) and
A8: r = (min ((min (f,g)),h,x,z)) . y by A5, FUNCT_1:def 3;
A9: [x,y] in [:C1,C2:] by A1, A7, ZFMISC_1:87;
(min ((min (f,g)),h,x,z)) . y = min (((min (f,g)) . [x,y]),(h . [y,z])) by A1, A2, A7, Def2
.= min ((min ((f . [x,y]),(g . [x,y]))),(h . [y,z])) by A9, FUZZY_1:def 3
.= min ((min ((h . [y,z]),(f . [x,y]))),(g . [x,y])) by XXREAL_0:33
.= min (((min (f,h,x,z)) . y),(g . [x,y])) by A1, A2, A7, Def2 ;
then r <= (min (f,h,x,z)) . y by A8, XXREAL_0:17;
hence ex y being set st
( y in dom (min ((min (f,g)),h,x,z)) & (upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= (min (f,h,x,z)) . y ) by A6, A7, XXREAL_0:2; :: thesis:

end;

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

let s be Real; :: thesis:
assume 0 < s ; :: thesis:
then consider r being Real such that
A11: r in rng (min ((min (f,g)),h,x,z)) and
A12: (upper_bound (rng (min ((min (f,g)),h,x,z)))) - s < r by A3, SEQ_4:def 1;
consider y being object such that
A13: y in dom (min ((min (f,g)),h,x,z)) and
A14: r = (min ((min (f,g)),h,x,z)) . y by A11, FUNCT_1:def 3;
A15: [x,y] in [:C1,C2:] by A1, A13, ZFMISC_1:87;
(min ((min (f,g)),h,x,z)) . y = min (((min (f,g)) . [x,y]),(h . [y,z])) by A1, A2, A13, Def2
.= min ((min ((f . [x,y]),(g . [x,y]))),(h . [y,z])) by A15, FUZZY_1:def 3
.= min ((f . [x,y]),(min ((h . [y,z]),(g . [x,y])))) by XXREAL_0:33
.= min (((min (g,h,x,z)) . y),(f . [x,y])) by A1, A2, A13, Def2 ;
then r <= (min (g,h,x,z)) . y by A14, XXREAL_0:17;
hence ex y being set st
( y in dom (min ((min (f,g)),h,x,z)) & (upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= (min (g,h,x,z)) . y ) by A12, A13, XXREAL_0:2; :: thesis:

end;

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 A16, SEQ_4:def 1; :: thesis:

end;

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

let s be Real; :: thesis:
assume 0 < s ; :: thesis:
then consider y being set such that
A18: y in dom (min ((min (f,g)),h,x,z)) and
A19: (upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= (min (g,h,x,z)) . y by A10;
y in C2 by A18;
then y in dom (min (g,h,x,z)) by FUNCT_2:def 1;
then (min (g,h,x,z)) . y <= upper_bound (rng (min (g,h,x,z))) by A17;
hence (upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= upper_bound (rng (min (g,h,x,z))) by A19, XXREAL_0:2; :: thesis:

end;

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 A21, SEQ_4:def 1; :: thesis:

end;

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

let s be Real; :: thesis:
assume 0 < s ; :: thesis:
then consider y being set such that
A23: y in dom (min ((min (f,g)),h,x,z)) and
A24: (upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= (min (f,h,x,z)) . y by A4;
y in C2 by A23;
then y in dom (min (f,h,x,z)) by FUNCT_2:def 1;
then (min (f,h,x,z)) . y <= upper_bound (rng (min (f,h,x,z))) by A22;
hence (upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= upper_bound (rng (min (f,h,x,z))) by A24, XXREAL_0:2; :: thesis:

end;