inferences in the axiomatic semantics

Hi:

The axiomatic semantics for DAML-ONT has a lot of statements of the form
Thn. <statement>.
However there are no derivations of these theorems.

I would find it very useful if we could see a full derivation of some of
these theorems.  I would suggest a couple of the domain and range theorems
for starters, perhaps for unionOf.  A derivation of a different sort of
theorem such as the one that cardinalities are non-negative and the one
that states that a minCardinality can be inferred from a hasValue would
also be useful to me.

Peter Patel-Schneider