Reqmnts, 2002

University of Bialystok

Copyright (c) 2002 Association of Mizar Users

### The abstract of the Mizar article:

### Boolean Properties of Sets --- Requirements

**by****Library Committee**- Received April 30, 2002
- MML identifier: BOOLE

- [ Mizar article, MML identifier index ]

environ vocabulary BOOLE; notation TARSKI, XBOOLE_0; constructors TARSKI, XBOOLE_0; clusters XBOOLE_0; begin :: This file contains statements which are obvious for Mizar checker if :: "requirements BOOLE" is included in the environment description :: of an article. They are published for testing purposes only. :: Users should use appropriate requirements instead of referencing :: to these theorems. :: Statements which cannot be expressed in Mizar language are commented out. theorem :: BOOLE:1 for X being set holds X \/ {} = X; theorem :: BOOLE:2 for X being set holds X /\ {} = {}; theorem :: BOOLE:3 for X being set holds X \ {} = X; theorem :: BOOLE:4 for X being set holds {} \ X = {}; theorem :: BOOLE:5 for X being set holds X \+\ {} = X; theorem :: BOOLE:6 for X being set st X is empty holds X = {}; theorem :: BOOLE:7 for x, X being set st x in X holds X is non empty; theorem :: BOOLE:8 for X, Y being set st X is empty & X <> Y holds Y is non empty; ::theorem :: equality of 0 and {} is assumed :: 0 is empty; ::theorem :: for X being set holds ::

Back to top numeral(X) & X <> 0 implies X is non empty;