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