[isabelle] On foundation axiom in ZF



First, I don't understand what square brackets here means:

definition
foundation_ax :: "(i=>o) => o" where
"foundation_ax(M) ==
∀x[M]. (∃y[M]. y∈x) --> (∃y[M]. y∈x & ~(∃z[M]. z∈x & z ∈ y))"

 
Please clarify.
 
Second, could you help to prove "not({t}: t)"?
 
--
Victor Porton - http://portonvictor.org


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