F₁() is CR from ABSRED_0:sch 9(A2, A3);
hence ( F₁() is SN & F₁() is CONF ) by A1, Lm1; :: according to ABSRED_0:def 28 :: thesis: verum