deffunc H₁( Subset of R, Subset of R) -> Element of [.0,1.] = kappa_2 ($1,$2);
for f1, f2 being Function of [:(bool the carrier of R),(bool the carrier of R):],[.0,1.] st ( for x, y being Subset of R holds f1 . (x,y) = H₁(x,y) ) & ( for x, y being Subset of R holds f2 . (x,y) = H₁(x,y) ) holds
f1 = f2 from ROUGHIF1:sch 1();
hence for b₁, b₂ being preRIF of R st ( for x, y being Subset of R holds b₁ . (x,y) = kappa_2 (x,y) ) & ( for x, y being Subset of R holds b₂ . (x,y) = kappa_2 (x,y) ) holds
b₁ = b₂ ; :: thesis: verum