:: Boolean Properties of Sets - Requirements
::  by Library Committee
::
:: Received April 30, 2002
:: Copyright (c) 2002 Association of Mizar Users

environ

 vocabularies BOOLE;
 notations 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
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;
    end;
    suppose x in {} & not x in X;
      hence thesis by XBOOLE_0:def 1;
    end;
  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;
  hence thesis by XBOOLE_0:def 2;
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
::    numeral(X) & X <> 0 implies X is non empty;