GFA0CarryOutput x,y,z in InnerVertices (BitGFA0Str x,y,z) by Th45;
hence [<*[<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ]*>,or3 ] is Element of InnerVertices (BitGFA0Str x,y,z) ; :: thesis: verum