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