defpred S₁[ set , set , set ] means $3 = upper_bound (rng (min h,g,$1,$2));
A1: for x, z, c1, c2 being set st x in C1 & z in C3 & S₁[x,z,c1] & S₁[x,z,c2] holds
c1 = c2 ;
A2: for x, z, c being set st x in C1 & z in C3 & S₁[x,z,c] holds
c in REAL ;
consider IT being PartFunc of [:C1,C3:],REAL such that
A3: ( ( for x, z being set holds
( [x,z] in dom IT iff ( x in C1 & z in C3 & ex c being set st S₁[x,z,c] ) ) ) & ( for x, z being set st [x,z] in dom IT holds
S₁[x,z,IT . x,z] ) ) from BINOP_1:sch 5(A2, A1);
A4: [:C1,C3:] c= dom IT

proof

let x, z be set ; :: according to RELAT_1:def 3 :: thesis: ( not [x,z] in [:C1,C3:] or [x,z] in dom IT )
A5: ex c being set st c = sup (rng (min h,g,x,z)) ;
assume A6: [x,z] in [:C1,C3:] ; :: thesis: [x,z] in dom IT
then A7: z in C3 by ZFMISC_1:106;
x in C1 by A6, ZFMISC_1:106;
hence [x,z] in dom IT by A3, A7, A5; :: thesis: verum

end;

then A8: dom IT = [:C1,C3:] by XBOOLE_0:def 10;
A9: dom IT = [:C1,C3:] by A4, XBOOLE_0:def 10;
rng IT c= [.0 ,1.]

proof

reconsider A = [.0 ,1.] as closed-interval Subset of REAL by INTEGRA1:def 1;
let c be set ; :: according to TARSKI:def 3 :: thesis: ( not c in rng IT or c in [.0 ,1.] )
assume c in rng IT ; :: thesis: c in [.0 ,1.]
then consider a being Element of [:C1,C3:] such that
a in dom IT and
A10: c = IT . a by PARTFUN1:26;
A11: A = [.(inf A),(sup A).] by INTEGRA1:5;
then A12: 0 = inf A by INTEGRA1:6;
A13: for x, z being set holds
( 0 <= sup (rng (min h,g,x,z)) & sup (rng (min h,g,x,z)) <= 1 )

proof

let x, z be set ; :: thesis: ( 0 <= sup (rng (min h,g,x,z)) & sup (rng (min h,g,x,z)) <= 1 )
A14: rng (min h,g,x,z) c= A by RELAT_1:def 19;
A is bounded_below by INTEGRA1:3;
then A15: inf A <= inf (rng (min h,g,x,z)) by A14, SEQ_4:64;
A is bounded_above by INTEGRA1:3;
then A16: sup (rng (min h,g,x,z)) <= sup A by A14, SEQ_4:65;
inf (rng (min h,g,x,z)) <= sup (rng (min h,g,x,z)) by Th1, SEQ_4:24;
hence ( 0 <= sup (rng (min h,g,x,z)) & sup (rng (min h,g,x,z)) <= 1 ) by A11, A16, A15, INTEGRA1:6; :: thesis: verum

end;

consider x, z being set such that
x in C1 and
z in C3 and
A17: a = [x,z] by ZFMISC_1:def 2;
A18: IT . x,z = sup (rng (min h,g,x,z)) by A3, A9, A17;
then A19: IT . a <= 1 by A13, A17;
A20: 1 = sup A by A11, INTEGRA1:6;
0 <= IT . a by A13, A17, A18;
hence c in [.0 ,1.] by A10, A12, A20, A19, INTEGRA2:1; :: thesis: verum

end;

then IT is RMembership_Func of C1,C3 by A8, FUNCT_2:def 1, RELAT_1:def 19;
hence ex b₁ being RMembership_Func of C1,C3 st
for x, z being set st [x,z] in [:C1,C3:] holds
b₁ . x,z = sup (rng (min h,g,x,z)) by A3, A8; :: thesis: verum