GFA1AdderOutput x,y,z in InnerVertices (BitGFA1Str x,y,z) by Th82;
hence 2GatesCircOutput x,y,z,xor2c is Element of InnerVertices (BitGFA1Str x,y,z) ; :: thesis: verum