GFA0AdderOutput (x,y,z) in InnerVertices (BitGFA0Str (x,y,z)) by Th37;
hence 2GatesCircOutput (x,y,z,xor2) is Element of InnerVertices (BitGFA0Str (x,y,z)) ; :: thesis: verum