GFA1CarryOutput (x,y,z) in InnerVertices (BitGFA1Str (x,y,z)) by Th69;
hence [<*[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]*>,or3] is Element of InnerVertices (BitGFA1Str (x,y,z)) ; :: thesis: verum