FDL > PVS > Graphs > doubletons > doubleton : type-eq-decl

doubleton : TYPE = {S | EXISTS x, y : (x /= y) AND (S = dbl(x, y))}