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

card(S): {(n:nat) | n = Card(S)} ;