:: Built-in Concepts
:: by Andrzej Trybulec
::
:: Received January 1, 1989
:: Copyright (c) 1990 Association of Mizar Users
begin
definition
mode
set
->
set
;
end;
definition
let
x
,
y
be
set
;
pred
x
=
y
;
reflexivity
errorfrm
;
symmetry
errorfrm
;
end;
notation
let
x
,
y
be
set
;
antonym
x
<>
y
for
x
=
y
;
end;
definition
let
x
,
X
be
set
;
pred
x
in
X
;
asymmetry
errorfrm
;
end;