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