The Mizar article:

Mizar Built-in Notions

by

Library Committee

Received January 1, 1989

Copyright (c) 1989 Association of Mizar Users

MML identifier: HIDDEN

[ 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;