let C1, C2, C3 be non empty set ; :: thesis: for f being RMembership_Func of C1,C2
for x, z being set st x in C1 & z in C3 holds
upper_bound (rng (min f,(Zmf C2,C3),x,z)) = (Zmf C1,C3) . [x,z]
let f be RMembership_Func of C1,C2; :: thesis: for x, z being set st x in C1 & z in C3 holds
upper_bound (rng (min f,(Zmf C2,C3),x,z)) = (Zmf C1,C3) . [x,z]
let x, z be set ; :: thesis: ( x in C1 & z in C3 implies upper_bound (rng (min f,(Zmf C2,C3),x,z)) = (Zmf C1,C3) . [x,z] )
assume that
A1: x in C1 and
A2: z in C3 ; :: thesis: upper_bound (rng (min f,(Zmf C2,C3),x,z)) = (Zmf C1,C3) . [x,z]
rng (min f,(Zmf C2,C3),x,z) is bounded by Th1;
then A3: rng (min f,(Zmf C2,C3),x,z) is bounded_above by XXREAL_2:def 11;
for s being real number st 0 < s holds
(upper_bound (rng (min f,(Zmf C2,C3),x,z))) - s <= (Zmf C1,C3) . [x,z]

proof

let s be real number ; :: thesis: ( 0 < s implies (upper_bound (rng (min f,(Zmf C2,C3),x,z))) - s <= (Zmf C1,C3) . [x,z] )
assume s > 0 ; :: thesis: (upper_bound (rng (min f,(Zmf C2,C3),x,z))) - s <= (Zmf C1,C3) . [x,z]
then consider r being real number such that
A4: r in rng (min f,(Zmf C2,C3),x,z) and
A5: (upper_bound (rng (min f,(Zmf C2,C3),x,z))) - s < r by A3, SEQ_4:def 4;
consider y being set such that
A6: y in dom (min f,(Zmf C2,C3),x,z) and
A7: r = (min f,(Zmf C2,C3),x,z) . y by A4, FUNCT_1:def 5;
A8: [y,z] in [:C2,C3:] by A2, A6, ZFMISC_1:106;
A9: [x,z] in [:C1,C3:] by A1, A2, ZFMISC_1:106;
A10: 0 <= f . [x,y] by Th3;
r = min (f . [x,y]),((Zmf C2,C3) . [y,z]) by A1, A2, A6, A7, Def2
.= min (f . [x,y]),0 by A8, FUNCT_3:def 3
.= 0 by A10, XXREAL_0:def 9
.= (Zmf C1,C3) . [x,z] by A9, FUNCT_3:def 3 ;
hence (upper_bound (rng (min f,(Zmf C2,C3),x,z))) - s <= (Zmf C1,C3) . [x,z] by A5; :: thesis: verum

end;

then A11: upper_bound (rng (min f,(Zmf C2,C3),x,z)) <= (Zmf C1,C3) . [x,z] by XREAL_1:59;
upper_bound (rng (min f,(Zmf C2,C3),x,z)) >= (Zmf C1,C3) . [x,z]

proof

reconsider A = [.0 ,1.] as closed-interval Subset of REAL by INTEGRA1:def 1;
A12: A is bounded_below by INTEGRA1:3;
rng (min f,(Zmf C2,C3),x,z) c= [.0 ,1.] by RELAT_1:def 19;
then A13: lower_bound A <= lower_bound (rng (min f,(Zmf C2,C3),x,z)) by A12, SEQ_4:64;
A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:5;
then A14: 0 = lower_bound A by INTEGRA1:6;
A15: lower_bound (rng (min f,(Zmf C2,C3),x,z)) <= upper_bound (rng (min f,(Zmf C2,C3),x,z)) by Th1, SEQ_4:24;
[x,z] in [:C1,C3:] by A1, A2, ZFMISC_1:106;
hence upper_bound (rng (min f,(Zmf C2,C3),x,z)) >= (Zmf C1,C3) . [x,z] by A14, A13, A15, FUNCT_3:def 3; :: thesis: verum

end;

hence upper_bound (rng (min f,(Zmf C2,C3),x,z)) = (Zmf C1,C3) . [x,z] by A11, XXREAL_0:1; :: thesis: verum