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