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