let n be Nat; :: thesis: for ap, bp, cp, dp being nonpair-yielding FinSequence holds InputVertices (n -BitFTA0Layer1Str (ap,bp,cp)) misses InnerVertices (n -BitFTA0Layer2Str (ap,bp,cp,dp))
let ap, bp, cp, dp be nonpair-yielding FinSequence; :: thesis: InputVertices (n -BitFTA0Layer1Str (ap,bp,cp)) misses InnerVertices (n -BitFTA0Layer2Str (ap,bp,cp,dp))
InputVertices (n -BitFTA0Layer1Str (ap,bp,cp)) is without_pairs by LmT0L1wp;
hence InputVertices (n -BitFTA0Layer1Str (ap,bp,cp)) misses InnerVertices (n -BitFTA0Layer2Str (ap,bp,cp,dp)) by FACIRC_1:5, LmT0L2rel; :: thesis: verum