[isabelle] A simple lemma


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

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.


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