The Mizar article:

Boolean Properties of Sets --- Requirements

by

Library Committee

Received April 30, 2002

Copyright (c) 2002 Association of Mizar Users

MML identifier: BOOLE

[ MML identifier index ]

environ

 vocabulary BOOLE;
 notation TARSKI, XBOOLE_0;
 constructors TARSKI, XBOOLE_0;
 clusters 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
::