GFA2AdderOutput x,y,z in InnerVertices (BitGFA2Str x,y,z) by Th119;
hence 2GatesCircOutput x,y,z,xor2c is Element of InnerVertices (BitGFA2Str x,y,z) ; :: thesis: verum