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