theorem :: GFACIRC1:131

for x, y, z being non pair set holds InputVertices (BitGFA3Str (x,y,z)) is without_pairs