[PVS-Help] Set clarification

[Jerome White <jerome@xxxxxxxxxxxxxx>]

The definition of min (from the prelude) is as follows:

  min(m, n): {p: real | p <= m AND p <= n}
    = IF m > n THEN n ELSE m ENDIF

where m and n are real numbers. My confusion is with respect to the
return type: it appears to me that min returns a set of real
numbers. Am I reading this correctly? If so, how is it that when used,
PVS knows the return type is a single value? For example

  min_le : LEMMA min(a,b) <= c IFF (a <= c OR b <= c)

Thanks

jerome