[isabelle] A set is not its own member



A problem about Isabelle/ZF:

I have a set Z and need to construct a set which is not a member of Z.

I heard that with the axiom of foundation (see ZF.thy) it can be proved
that any set is not member of itself. (This solves the above stated
problem.)

Could anyone guid me how I can prove that a set is not its own member in
Isabelle/ZF.

(I am an Isabelle novice but developing a theory which will
revolutionarize further development of formal proof assistants based on
ZF. Please help me to accomplish this task.)

-- 
Victor Porton - http://portonvictor.org






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