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