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;