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