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