let C1, C2, C3 be non empty set ; :: thesis: for f being RMembership_Func of C1,C2
for g being RMembership_Func of C2,C3
for x, z being set st x in C1 & z in C3 holds
sup (rng (min (converse g),(converse f),z,x)) = sup (rng (min f,g,x,z))
let f be RMembership_Func of C1,C2; :: thesis: for g being RMembership_Func of C2,C3
for x, z being set st x in C1 & z in C3 holds
sup (rng (min (converse g),(converse f),z,x)) = sup (rng (min f,g,x,z))
let g be RMembership_Func of C2,C3; :: thesis: for x, z being set st x in C1 & z in C3 holds
sup (rng (min (converse g),(converse f),z,x)) = sup (rng (min f,g,x,z))
let x, z be set ; :: thesis: ( x in C1 & z in C3 implies sup (rng (min (converse g),(converse f),z,x)) = sup (rng (min f,g,x,z)) )
assume A1: ( x in C1 & z in C3 ) ; :: thesis: sup (rng (min (converse g),(converse f),z,x)) = sup (rng (min f,g,x,z))
A2: sup (rng (min (converse g),(converse f),z,x)) <= sup (rng (min f,g,x,z))

proof

rng (min (converse g),(converse f),z,x) is bounded by Th1;
then A3: rng (min (converse g),(converse f),z,x) is bounded_above by XXREAL_2:def 11;
for s being real number st 0 < s holds
(sup (rng (min (converse g),(converse f),z,x))) - s <= sup (rng (min f,g,x,z))

proof

let s be real number ; :: thesis: ( 0 < s implies (sup (rng (min (converse g),(converse f),z,x))) - s <= sup (rng (min f,g,x,z)) )
assume s > 0 ; :: thesis: (sup (rng (min (converse g),(converse f),z,x))) - s <= sup (rng (min f,g,x,z))
then consider r being real number such that
A4: ( r in rng (min (converse g),(converse f),z,x) & (sup (rng (min (converse g),(converse f),z,x))) - s < r ) by A3, SEQ_4:def 4;
consider y being set such that
A5: ( y in dom (min (converse g),(converse f),z,x) & r = (min (converse g),(converse f),z,x) . y ) by A4, FUNCT_1:def 5;
y in C2 by A5;
then A6: ( [z,y] in [:C3,C2:] & [y,x] in [:C2,C1:] & y in dom (min f,g,x,z) ) by A1, FUNCT_2:def 1, ZFMISC_1:106;
then A7: (min f,g,x,z) . y <= sup (rng (min f,g,x,z)) by Th1;
r = min ((converse g) . z,y),((converse f) . y,x) by A1, A5, Def2
.= min (g . y,z),((converse f) . y,x) by A6, Def1
.= min (g . y,z),(f . x,y) by A6, Def1
.= (min f,g,x,z) . y by A1, A5, Def2 ;
hence (sup (rng (min (converse g),(converse f),z,x))) - s <= sup (rng (min f,g,x,z)) by A4, A7, XXREAL_0:2; :: thesis: verum

end;

hence sup (rng (min (converse g),(converse f),z,x)) <= sup (rng (min f,g,x,z)) by XREAL_1:59; :: thesis: verum

end;

sup (rng (min (converse g),(converse f),z,x)) >= sup (rng (min f,g,x,z))

proof

rng (min f,g,x,z) is bounded by Th1;
then A8: rng (min f,g,x,z) is bounded_above by XXREAL_2:def 11;
for s being real number st 0 < s holds
(sup (rng (min f,g,x,z))) - s <= sup (rng (min (converse g),(converse f),z,x))

proof

let s be real number ; :: thesis: ( 0 < s implies (sup (rng (min f,g,x,z))) - s <= sup (rng (min (converse g),(converse f),z,x)) )
assume s > 0 ; :: thesis: (sup (rng (min f,g,x,z))) - s <= sup (rng (min (converse g),(converse f),z,x))
then consider r being real number such that
A9: ( r in rng (min f,g,x,z) & (sup (rng (min f,g,x,z))) - s < r ) by A8, SEQ_4:def 4;
consider y being set such that
A10: ( y in dom (min f,g,x,z) & r = (min f,g,x,z) . y ) by A9, FUNCT_1:def 5;
y in C2 by A10;
then A11: ( [z,y] in [:C3,C2:] & [y,x] in [:C2,C1:] & y in dom (min (converse g),(converse f),z,x) ) by A1, FUNCT_2:def 1, ZFMISC_1:106;
then A12: (min (converse g),(converse f),z,x) . y <= sup (rng (min (converse g),(converse f),z,x)) by Th1;
r = min (f . x,y),(g . y,z) by A1, A10, Def2
.= min ((converse f) . y,x),(g . y,z) by A11, Def1
.= min ((converse f) . y,x),((converse g) . z,y) by A11, Def1
.= (min (converse g),(converse f),z,x) . y by A1, A10, Def2 ;
hence (sup (rng (min f,g,x,z))) - s <= sup (rng (min (converse g),(converse f),z,x)) by A9, A12, XXREAL_0:2; :: thesis: verum

end;

hence sup (rng (min (converse g),(converse f),z,x)) >= sup (rng (min f,g,x,z)) by XREAL_1:59; :: thesis: verum

end;

hence sup (rng (min (converse g),(converse f),z,x)) = sup (rng (min f,g,x,z)) by A2, XXREAL_0:1; :: thesis: verum