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