:: Boolean Properties of Sets - Requirements :: by Library Committee :: :: Received April 30, 2002 :: Copyright (c) 2002-2019 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;