FDL > PVS > Finite Sets > card def > Card : const-decl

Card(S): nat = min(inj set(S));