Copyright (c) 2002 Association of Mizar Users
environ vocabulary BOOLE; notation TARSKI, XBOOLE_0; constructors TARSKI, XBOOLE_0; definitions XBOOLE_0, TARSKI; theorems 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 for X being set holds X \/ {} = X proof let X be set; thus X \/ {} c= X proof let x be set; assume x in X \/ {}; then x in X or x in {} by XBOOLE_0:def 2; hence thesis by XBOOLE_0:def 1; end; let x be set; assume x in X; hence thesis by XBOOLE_0:def 2; end; theorem for X being set holds X /\ {} = {} proof let X be set; thus X /\ {} c= {} proof let x be set; assume x in X /\ {}; hence thesis by XBOOLE_0:def 3; end; let x be set; 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 set; assume x in X \ {}; hence thesis by XBOOLE_0:def 4; end; let x be set; assume x in X; then x in X & not x in {} by XBOOLE_0:def 1; hence thesis by XBOOLE_0:def 4; end; theorem for X being set holds {} \ X = {} proof let X be set; thus {} \ X c= {} proof let x be set; assume x in {} \ X; hence thesis by XBOOLE_0:def 4; end; let x be set; 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 set; assume x in X \+\ {}; then x in (X \ {}) \/ ({} \ X) by XBOOLE_0:def 6; then A1: x in X \ {} or x in {} \ X by XBOOLE_0:def 2; per cases by A1,XBOOLE_0:def 4; suppose x in X & not x in {}; hence thesis; suppose x in {} & not x in X; hence thesis by XBOOLE_0:def 1; end; let x be set; assume x in X; then x in X & not x in {} by XBOOLE_0:def 1; then x in X \ {} by XBOOLE_0:def 4; then x in (X \ {}) \/ ({} \ X) by XBOOLE_0:def 2; hence thesis by XBOOLE_0:def 6; end; theorem for X being set st X is empty holds X = {} by XBOOLE_0:def 5; theorem for x, X being set st x in X holds X is non empty proof let x, X be set; assume x in X; then X <> {} by XBOOLE_0:def 1; hence thesis by XBOOLE_0:def 5; end; 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,XBOOLE_0:def 5; hence thesis by A2,XBOOLE_0:def 5; end; ::theorem :: equality of 0 and {} is assumed :: 0 is empty; ::theorem :: for X being set holds ::