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