GFA3AdderOutput (x,y,z) in InnerVertices (BitGFA3Str (x,y,z)) by Th133;
hence 2GatesCircOutput (x,y,z,xor2) is Element of InnerVertices (BitGFA3Str (x,y,z)) ; :: thesis: verum