:: Boolean Properties of Sets - Requirements :: by Library Committee :: :: Received April 30, 2002 :: Copyright (c) 2002-2018 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; definitions XBOOLE_0, TARSKI; equalities XBOOLE_0; expansions TARSKI; theorems XBOOLE_0, TARSKI; 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 for X being set holds X \/ {} = X proof let X be set; thus X \/ {} c= X proof let x be object; assume x in X \/ {}; then x in X or x in {} by XBOOLE_0:def 3; hence thesis by XBOOLE_0:def 1; end; let x be object; assume x in X; hence thesis by XBOOLE_0:def 3; end; theorem for X being set holds X /\ {} = {} proof let X be set; thus X /\ {} c= {} by XBOOLE_0:def 4; let x be object; assume x in {}; hence thesis by XBOOLE_0:def 1; end; theorem for X being set holds X \ {} = X proof let X be set; thus X \ {} c= X by XBOOLE_0:def 5; let x be object; A1: not x in {} by XBOOLE_0:def 1; assume x in X; hence thesis by A1,XBOOLE_0:def 5; end; theorem for X being set holds {} \ X = {} proof let X be set; thus {} \ X c= {} by XBOOLE_0:def 5; let x be object; assume x in {}; hence thesis by XBOOLE_0:def 1; end; theorem for X being set holds X \+\ {} = X proof let X be set; thus X \+\ {} c= X proof let x be object; assume x in X \+\ {}; then A1: x in X \ {} or x in {} \ X by XBOOLE_0:def 3; per cases by A1,XBOOLE_0:def 5; suppose x in X & not x in {}; hence thesis; end; suppose x in {} & not x in X; hence thesis by XBOOLE_0:def 1; end; end; let x be object; A2: not x in {} by XBOOLE_0:def 1; assume x in X; then x in X \ {} by A2,XBOOLE_0:def 5; hence thesis by XBOOLE_0:def 3; end; reserve x,X for set; Lm1: X is empty implies X = {} proof assume not ex x being object st x in X; then for x being object holds x in {} iff x in X by XBOOLE_0:def 1; hence thesis by TARSKI:2; end; theorem for X being set st X is empty holds X = {} by Lm1; theorem for x, X being set st x in X holds X is non empty by XBOOLE_0:def 1; theorem for X, Y being set st X is empty & X <> Y holds Y is non empty proof let X, Y be set; assume that A1: X is empty and A2: X <> Y; X = {} by A1,Lm1; hence thesis by A2,Lm1; end; ::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;