Journal of Formalized Mathematics
Axiomatics, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

The abstract of the Mizar article:

Mizar Built-in Notions

by
Library Committee

Received January 1, 1989

MML identifier: HIDDEN
[ Mizar article, MML identifier index ]


environ



begin

definition
  mode set;
end;

definition let x,y be set;
  pred x = y;
   reflexivity;
   symmetry;
  antonym x <> y;
end;

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

Back to top