deffunc H₁( Subset of R, Subset of R) -> Element of [.0,1.] = In (((((CMap (kappa R)) . ($1,$2)) + ((CMap (kappa R)) . ($2,$1))) / 2),[.0,1.]);
ex f being preRIF of R st
for x, y being Element of bool the carrier of R holds f . (x,y) = H₁(x,y) from BINOP_1:sch 4();
then consider ff being Function of [:(bool the carrier of R),(bool the carrier of R):],[.0,1.] such that
A1: for x, y being Element of bool the carrier of R holds ff . (x,y) = H₁(x,y) ;
take ff ; :: thesis: for x, y being Subset of R holds ff . (x,y) = (((CMap (kappa R)) . (x,y)) + ((CMap (kappa R)) . (y,x))) / 2
let x, y be Subset of R; :: thesis: ff . (x,y) = (((CMap (kappa R)) . (x,y)) + ((CMap (kappa R)) . (y,x))) / 2
b1: ( 0 <= (CMap (kappa R)) . (x,y) & 0 <= (CMap (kappa R)) . (y,x) ) by XXREAL_1:1;
( (CMap (kappa R)) . (x,y) <= 1 & (CMap (kappa R)) . (y,x) <= 1 ) by XXREAL_1:1;
then ((CMap (kappa R)) . (x,y)) + ((CMap (kappa R)) . (y,x)) <= 1 + 1 by XREAL_1:7;
then bb: (((CMap (kappa R)) . (x,y)) + ((CMap (kappa R)) . (y,x))) / 2 <= 2 / 2 by XREAL_1:72;
ff . (x,y) = In (((((CMap (kappa R)) . (x,y)) + ((CMap (kappa R)) . (y,x))) / 2),[.0,1.]) by A1
.= (((CMap (kappa R)) . (x,y)) + ((CMap (kappa R)) . (y,x))) / 2 by bb, SUBSET_1:def 8, b1, XXREAL_1:1 ;
hence ff . (x,y) = (((CMap (kappa R)) . (x,y)) + ((CMap (kappa R)) . (y,x))) / 2 ; :: thesis: verum