set M = ModelSP (Inf_seq S);
deffunc H1( Element of ModelSP (Inf_seq S), Element of ModelSP (Inf_seq S)) -> Element of ModelSP (Inf_seq S) = (Not_ S) . ((Until_ S) . (((Not_ S) . $1),((Not_ S) . $2)));
consider o being BinOp of (ModelSP (Inf_seq S)) such that
A2:
for f, g being Element of ModelSP (Inf_seq S) holds o . (f,g) = H1(f,g)
from BINOP_1:sch 4();
for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds
o . (f,g) = (Not_ S) . ((Until_ S) . (((Not_ S) . f),((Not_ S) . g)))
by A2;
hence
ex b1 being BinOp of (ModelSP (Inf_seq S)) st
for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds
b1 . (f,g) = (Not_ S) . ((Until_ S) . (((Not_ S) . f),((Not_ S) . g)))
; verum