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