[mizar] HIDDEN

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

Hi:

There is this definition in HIDDEN

definition let x,X be set;
 pred x in X;
  antisymmetry;
end;

Aside of the problem that the meant property be better named asymmetry,
there is also some redundance here.  Namely, that x in X is 
asymmetric follows from the regularity axiom and thus we should have 
x in X defined as

definition let x,X be set;
 pred x in X;
end;

or to be faceciuos even as

definition let x,X be set;
 pred x in X means
 not contradiction;
end;

and then, only after regularity we should

definition let x,X be set;
 redefine pred x in X;
  antisymmetry;
end;

Similar things can be done for mode set and pred x = y, and then
HIDDEN could be eliminated.

-- 
Piotr Rudnicki               CompSci, Univerity of Alberta, Edmonton, Canada
email: piotr@cs.ualberta.ca                 http://web.cs.ualberta.ca/~piotr