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

proof

let x, z be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,z] in [:C1,C3:] or [x,z] in dom IT )
A5: upper_bound (rng (min (h,g,x,z))) is set by TARSKI:1;
assume A6: [x,z] in [:C1,C3:] ; :: thesis: [x,z] in dom IT
then A7: z in C3 by ZFMISC_1:87;
x in C1 by A6, ZFMISC_1:87;
hence [x,z] in dom IT by A3, A5, A7; :: thesis: verum

end;

then A8: dom IT = [:C1,C3:] ;
rng IT c= [.0,1.]

proof

reconsider A = [.0,jj.] as non empty closed_interval Subset of REAL by MEASURE5:14;
let c be object ; :: 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:3;
A11: A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then A12: 0 = lower_bound A by INTEGRA1:5;
A13: for x, z being set holds
( 0 <= upper_bound (rng (min (h,g,x,z))) & upper_bound (rng (min (h,g,x,z))) <= 1 )

proof

let x, z be set ; :: thesis: ( 0 <= upper_bound (rng (min (h,g,x,z))) & upper_bound (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: lower_bound A <= lower_bound (rng (min (h,g,x,z))) by A14, SEQ_4:47;
A is bounded_above by INTEGRA1:3;
then A16: upper_bound (rng (min (h,g,x,z))) <= upper_bound A by A14, SEQ_4:48;
lower_bound (rng (min (h,g,x,z))) <= upper_bound (rng (min (h,g,x,z))) by Th1, SEQ_4:11;
hence ( 0 <= upper_bound (rng (min (h,g,x,z))) & upper_bound (rng (min (h,g,x,z))) <= 1 ) by A11, A16, A15, INTEGRA1:5; :: thesis: verum

end;

consider x, z being object such that
x in C1 and
z in C3 and
A17: a = [x,z] by ZFMISC_1:def 2;
reconsider z = z, x = x as set by TARSKI:1;
A18: IT . (x,z) = upper_bound (rng (min (h,g,x,z))) by A3, A8, A17;
then A19: IT . a <= 1 by A13, A17;
A20: 1 = upper_bound A by A11, INTEGRA1:5;
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 object st [x,z] in [:C1,C3:] holds
b₁ . (x,z) = upper_bound (rng (min (h,g,x,z))) by A3, A8; :: thesis: verum