:: Boolean Properties of Sets - Requirements
:: by Library Committee
::
:: Received April 30, 2002
:: Copyright (c) 2002-2012 Association of Mizar Users


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
proof end;

theorem :: BOOLE:2
for X being set holds X /\ {} = {}
proof end;

theorem :: BOOLE:3
for X being set holds X \ {} = X
proof end;

theorem :: BOOLE:4
for X being set holds {} \ X = {}
proof end;

theorem :: BOOLE:5
for X being set holds X \+\ {} = X
proof end;

Lm1: for X being set st X is empty holds
X = {}
proof end;

theorem :: BOOLE:6
for X being set st X is empty holds
X = {} by Lm1;

theorem :: BOOLE:7
for x, X being set st x in X holds
not X is empty by XBOOLE_0:def 1;

theorem :: BOOLE:8
for X, Y being set st X is empty & X <> Y holds
not Y is empty
proof end;