set II = U -InterpretersOf S;
set AF = AtomicFormulasOf S;
deffunc H₁( Element of U -InterpretersOf S, Element of AtomicFormulasOf S) -> Element of BOOLEAN = $1 -AtomicEval $2;
consider f being Function of [:(U -InterpretersOf S),(AtomicFormulasOf S):],BOOLEAN such that
A1: for I being Element of U -InterpretersOf S
for phi being Element of AtomicFormulasOf S holds f . (I,phi) = H₁(I,phi) from BINOP_1:sch 4();
take f ; :: thesis: for I being Element of U -InterpretersOf S
for phi being Element of AtomicFormulasOf S holds f . (I,phi) = I -AtomicEval phi
thus for I being Element of U -InterpretersOf S
for phi being Element of AtomicFormulasOf S holds f . (I,phi) = I -AtomicEval phi by A1; :: thesis: verum