let C1, C2, C3 be non empty set ; :: thesis:
let f, g be RMembership_Func of C1,C2; :: thesis:
let h, k be RMembership_Func of C2,C3; :: thesis:
let x, z be set ; :: thesis:
assume that
A1: x in C1 and
A2: z in C3 and
A3: for y being set st y in C2 holds
( f . [x,y] <= g . [x,y] & h . [y,z] <= k . [y,z] ) ; :: thesis:
A4: [x,z] in [:C1,C3:] by A1, A2, ZFMISC_1:87;
then A5: (g (#) k) . (x,z) = upper_bound (rng (min (g,k,x,z))) by Def3;
rng (min (f,h,x,z)) is real-bounded by Th1;
then A6: rng (min (f,h,x,z)) is bounded_above by XXREAL_2:def 11;
A7: for s being Real st s > 0 holds
(upper_bound (rng (min (f,h,x,z)))) - s <= upper_bound (rng (min (g,k,x,z)))

proof

let s be Real; :: thesis:
assume s > 0 ; :: thesis:
then consider r being Real such that
A8: r in rng (min (f,h,x,z)) and
A9: (upper_bound (rng (min (f,h,x,z)))) - s < r by A6, SEQ_4:def 1;
consider y being object such that
A10: y in dom (min (f,h,x,z)) and
A11: r = (min (f,h,x,z)) . y by A8, FUNCT_1:def 3;
A12: h . [y,z] <= k . [y,z] by A3, A10;
f . [x,y] <= g . [x,y] by A3, A10;
then min ((f . [x,y]),(h . [y,z])) <= min ((g . [x,y]),(k . [y,z])) by A12, XXREAL_0:18;
then A13: (min (f,h,x,z)) . y <= min ((g . [x,y]),(k . [y,z])) by A1, A2, A10, Def2;
y in C2 by A10;
then A14: y in dom (min (g,k,x,z)) by FUNCT_2:def 1;
min ((g . [x,y]),(k . [y,z])) = (min (g,k,x,z)) . y by A1, A2, A10, Def2;
then min ((g . [x,y]),(k . [y,z])) <= upper_bound (rng (min (g,k,x,z))) by A14, Th1;
then (min (f,h,x,z)) . y <= upper_bound (rng (min (g,k,x,z))) by A13, XXREAL_0:2;
hence (upper_bound (rng (min (f,h,x,z)))) - s <= upper_bound (rng (min (g,k,x,z))) by A9, A11, XXREAL_0:2; :: thesis:

end;

(f (#) h) . (x,z) = upper_bound (rng (min (f,h,x,z))) by A4, Def3;
hence (f (#) h) . [x,z] <= (g (#) k) . [x,z] by A5, A7, XREAL_1:57; :: thesis: