GFA2CarryOutput (x,y,z) in InnerVertices (BitGFA2Str (x,y,z)) by Th101;
hence [<*[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,nor2]*>,nor3] is Element of InnerVertices (BitGFA2Str (x,y,z)) ; :: thesis: verum