[PVS-Help] Using THEOREM in proof

[leila@xxxxxxxxxxxx]

Hi

I am trying to use the THEOREMs defined in the finite_sets theory
associated with the cardinalities.

Unfortunately I am unable to find how to use these THEOREMs. I am trying
to prove LEMMATA like this simplified test example:

card(S) = 0 => empty(S)

This is a lot like the empty_card THEOREM.and card_empty? THEOREM. Can
someone help me to complete this example proof?

Kind regards

Christian