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