let x, y, z be non pair set ; :: thesis: InputVertices (BitGFA3Str (x,y,z)) is without_pairs
InputVertices (BitGFA3Str (x,y,z)) = {x,y,z} by Th130;
hence InputVertices (BitGFA3Str (x,y,z)) is without_pairs ; :: thesis: verum