:: Boolean Properties of Sets - Requirements
:: by Library Committee
::
:: Received April 30, 2002
:: Copyright (c) 2002-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, TARSKI;
notations TARSKI, XBOOLE_0;
constructors TARSKI, 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;
reserve x,X for set;
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
:: numeral(X) & X <> 0 implies X is non empty;