deffunc H₁( Element of Topology_of T, Element of Topology_of T) -> Element of Topology_of T = $1 \/ $2;
thus ex F being BinOp of (Topology_of T) st
for P, Q being Element of Topology_of T holds F . (P,Q) = H₁(P,Q) from BINOP_1:sch 4(); :: thesis: verum