set A = [.0,1.];
deffunc H₁( Element of [.0,1.], Element of [.0,1.]) -> Element of [.0,1.] = In ((max ($2,(min ((1 - $1),(1 - $2))))),[.0,1.]);
ex f being Function of [:[.0,1.],[.0,1.]:],[.0,1.] st
for x, y being Element of [.0,1.] holds f . (x,y) = H₁(x,y) from BINOP_1:sch 4();
then consider f being BinOp of [.0,1.] such that
A1: for x, y being Element of [.0,1.] holds f . (x,y) = H₁(x,y) ;
take f ; :: thesis: for x, y being Element of [.0,1.] holds f . (x,y) = max (y,(min ((1 - x),(1 - y))))
let a, b be Element of [.0,1.]; :: thesis: f . (a,b) = max (b,(min ((1 - a),(1 - b))))
f . (a,b) = H₁(a,b) by A1;
hence f . (a,b) = max (b,(min ((1 - a),(1 - b)))) by SUBSET_1:def 8, MaxMinIn01; :: thesis: verum