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