Re: [mizar] Isn't "Subset of" the same as "Element of bool"?

[Adam Naumowicz <adamn@math.uwb.edu.pl>]

Dear Freek,

On Tue, 28 Jan 2003, Freek Wiedijk wrote:

I'm not sure whether it is exactly what you want, but I would write it as
follows:

environ
 notation ZFMISC_1, SUBSET_1;
 constructors TARSKI, SUBSET_1;
 theorems ZFMISC_1;
 clusters SUBSET_1;
 requirements SUBSET;
begin

:: Subset of A -> Subset of B

definition
 let O be set;
 let A be Subset of O;
 mode Subset of A is Element of bool O;
end;

for B being set, A being Subset of B, X being Subset of A holds
 X qua Subset of B is set;


Adam Naumowicz

======================================================================
Department of Applied Logic            fax. +48 (85) 745-7662
Institute of Computer Science          tel. +48 (85) 745-7559 (office)
University of Bialystok                e-mail: adamn@mizar.org
Sosnowa 64, 15-887 Bialystok, Poland   http://math.uwb.edu.pl/~adamn/
======================================================================