# Re: [isabelle] Proving cardinality

```How about

definition S :: "nat set" where
"S ≡ {1,2}"

lemma "card S > 1"

```
The same should work with your axiomatic version (but I don't see why you would use an axiom in this case). Just give the equation of the axiom an explicit name and supply it to simp.
```
Maybe a nicer way to state S would be

context
fixes S :: "nat set"
assumes S_def: "S = {1, 2}"
begin

lemma "card S > 1"

end

cheers

chris

On 07/25/2012 08:55 AM, John Munroe wrote:
```
```Hi,

I'm trying to prove the cardinality of the set {1,2} being greater
than 1, but I seem to be able to only prove that the cardinality is
greater than 0:

axiomatization
S :: "nat set" where
ax1 : "S = {1,2}"

lemma "card S > 0"
using ax1
by (metis card_eq_0_iff finite.emptyI finite.insertI gr0I insert_not_empty)

Now I'm trying to prove:

lemma "card S > 1"
sledgehammer

Thanks a lot for your time.

John

```
```

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.