thus for t being bin-term holds S₁[t] from BINTREE1:sch 2(Lm7, Lm8); :: thesis: verum