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
::