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