[isabelle] A simple lemma



Hi,

I'm having trouble proving the following, could someone please help?

axiomatization
T :: "real set" and
S :: "real set" where
ax1: "T = {1,2}" and
ax2: "S = {1,2,3}"

lemma "ALL t:T. EX s : S. even t <-> s*t=6"

I expect it to be true since only 2 in T is even.

Any help will be appreciated. Thanks.

John





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