deffunc H_{1}( 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_{1}(P,Q)
from BINOP_1:sch 4(); :: thesis: verum

thus ex F being BinOp of (Topology_of T) st

for P, Q being Element of Topology_of T holds F . (P,Q) = H