let n be Nat; :: thesis: for ap, bm, cp, dm being nonpair-yielding FinSequence holds InputVertices (n -BitFTA1Layer1Str (ap,bm,cp)) misses InnerVertices (n -BitFTA1Layer2Str (ap,bm,cp,dm))
let ap, bm, cp, dm be nonpair-yielding FinSequence; :: thesis: InputVertices (n -BitFTA1Layer1Str (ap,bm,cp)) misses InnerVertices (n -BitFTA1Layer2Str (ap,bm,cp,dm))
InputVertices (n -BitFTA1Layer1Str (ap,bm,cp)) is without_pairs by LmT1L1wp;
hence InputVertices (n -BitFTA1Layer1Str (ap,bm,cp)) misses InnerVertices (n -BitFTA1Layer2Str (ap,bm,cp,dm)) by FACIRC_1:5, LmT1L2rel; :: thesis: verum