The abstract of the Mizar article:

Boolean Domains

by

Andrzej Trybulec, and

Agata Darmochwal

Received April 14, 1989

MML identifier: FINSUB_1

[ Mizar article, MML identifier index ]

environ

 vocabulary BOOLE, FINSET_1, FINSUB_1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1;
 constructors TARSKI, SUBSET_1, FINSET_1, XBOOLE_0;
 clusters FINSET_1, SUBSET_1, XBOOLE_0, ZFMISC_1;
 requirements SUBSET, BOOLE;


begin

:::::::::::::: Auxiliary theorems :::::::::::::::::::

reserve X,Y for set;

definition let IT be set;
  attr IT is cup-closed means
:: FINSUB_1:def 1
   for X,Y being set st X in IT & Y in IT holds X \/ Y in IT;
  attr IT is cap-closed means
:: FINSUB_1:def 2
     for X,Y being set st X in IT & Y in IT holds X /\ Y in IT;
  attr IT is diff-closed means
:: FINSUB_1:def 3
   for X,Y being set st X in IT & Y in IT holds X \ Y in IT;
end;

definition let IT be set;
  attr IT is preBoolean means
:: FINSUB_1:def 4
   IT is cup-closed diff-closed;
end;

definition
  cluster preBoolean -> cup-closed diff-closed set;
  cluster cup-closed diff-closed -> preBoolean set;
end;

definition
 cluster non empty cup-closed cap-closed diff-closed set;
end;

reserve A for non empty preBoolean set;

canceled 9;

theorem :: FINSUB_1:10
 for A being set holds A is preBoolean iff
  for X,Y being set st X in A & Y in A holds X \/ Y in A & X \ Y in A;

definition let A; let X,Y be Element of A;
 redefine func X \/ Y -> Element of A;
  func X \ Y -> Element of A;
end;

canceled 2;

theorem :: FINSUB_1:13
 X is Element of A & Y is Element of A implies X /\ Y is Element of A;

theorem :: FINSUB_1:14
 X is Element of A & Y is Element of A implies X \+\ Y is Element of A;

theorem :: FINSUB_1:15
   for A being non empty set st
   for X,Y being Element of A holds X \+\ Y in A & X \ Y in A
  holds A is preBoolean;

theorem :: FINSUB_1:16
   for A being non empty set st
   for X,Y being Element of A holds X \+\ Y in A & X /\ Y in A
  holds A is preBoolean;

theorem :: FINSUB_1:17
   for A being non empty set st
   for X,Y being Element of A holds X \+\ Y in A & X \/ Y in A
  holds A is preBoolean;

definition let A; let X,Y be Element of A;
 redefine func X /\ Y -> Element of A;
  func X \+\ Y -> Element of A;
end;

theorem :: FINSUB_1:18
 {} in A;

canceled;

theorem :: FINSUB_1:20
  for A being set holds bool A is preBoolean;

theorem :: FINSUB_1:21
   for A,B being non empty preBoolean set holds A /\ B is non empty preBoolean;

 reserve A,B,P for set;
 reserve x for set;

:::::::::::::: The set of all finite subsets of a set ::::::::::::::::

definition let A;
 func Fin A -> preBoolean set means
:: FINSUB_1:def 5
   for X being set holds X in it iff X c= A & X is finite;
 end;

definition let A;
 cluster Fin A -> non empty;
end;

definition let A;
 cluster -> finite Element of Fin A;
end;

canceled;

theorem :: FINSUB_1:23
 A c= B implies Fin A c= Fin B;

theorem :: FINSUB_1:24
   Fin (A /\ B) = Fin A /\ Fin B;

theorem :: FINSUB_1:25
   Fin A \/ Fin B c= Fin (A \/ B);

theorem :: FINSUB_1:26
 Fin A c= bool A;

theorem :: FINSUB_1:27
 A is finite implies Fin A = bool A;

theorem :: FINSUB_1:28
   Fin {} = { {} };

:::::::::::::: Finite subsets ::::::::::::::::

definition let A;
  mode Finite_Subset of A is Element of Fin A;
end;

canceled;

theorem :: FINSUB_1:30
   for X being Finite_Subset of A holds X is finite;

canceled;

theorem :: FINSUB_1:32
   for X being Finite_Subset of A holds X is Subset of A;

canceled;

theorem :: FINSUB_1:34
   A is finite implies
  for X being Subset of A holds X is Finite_Subset of A;