:: by Andrzej Trybulec and Agata Darmochwa\l

::

:: Received April 14, 1989

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

definition

let IT be set ;

end;
attr IT is cup-closed means :Def1: :: FINSUB_1:def 1

for X, Y being set st X in IT & Y in IT holds

X \/ Y in IT;

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;

for X, Y being set st X in IT & Y in IT holds

X /\ Y in IT;

attr IT is diff-closed means :Def3: :: FINSUB_1:def 3

for X, Y being set st X in IT & Y in IT holds

X \ Y in IT;

for X, Y being set st X in IT & Y in IT holds

X \ Y in IT;

:: deftheorem Def1 defines cup-closed FINSUB_1:def 1 :

for IT being set holds

( IT is cup-closed iff for X, Y being set st X in IT & Y in IT holds

X \/ Y in IT );

for IT being set holds

( IT is cup-closed iff for X, Y being set st X in IT & Y in IT holds

X \/ Y in IT );

:: deftheorem defines cap-closed FINSUB_1:def 2 :

for IT being set holds

( IT is cap-closed iff for X, Y being set st X in IT & Y in IT holds

X /\ Y in IT );

for IT being set holds

( IT is cap-closed iff for X, Y being set st X in IT & Y in IT holds

X /\ Y in IT );

:: deftheorem Def3 defines diff-closed FINSUB_1:def 3 :

for IT being set holds

( IT is diff-closed iff for X, Y being set st X in IT & Y in IT holds

X \ Y in IT );

for IT being set holds

( IT is diff-closed iff for X, Y being set st X in IT & Y in IT holds

X \ Y in IT );

:: deftheorem Def4 defines preBoolean FINSUB_1:def 4 :

for IT being set holds

( IT is preBoolean iff ( IT is cup-closed & IT is diff-closed ) );

for IT being set holds

( IT is preBoolean iff ( IT is cup-closed & IT is diff-closed ) );

registration

coherence

for b_{1} being set st b_{1} is preBoolean holds

( b_{1} is cup-closed & b_{1} is diff-closed )
by Def4;

coherence

for b_{1} being set st b_{1} is cup-closed & b_{1} is diff-closed holds

b_{1} is preBoolean
by Def4;

end;
for b

( b

coherence

for b

b

registration

existence

ex b_{1} being set st

( not b_{1} is empty & b_{1} is cup-closed & b_{1} is cap-closed & b_{1} is diff-closed )

end;
ex b

( not b

proof end;

theorem Th1: :: FINSUB_1:1

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 ) )

( 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 ) )

proof end;

definition

let A be non empty preBoolean set ;

let X, Y be Element of A;

:: original: \/

redefine func X \/ Y -> Element of A;

correctness

coherence

X \/ Y is Element of A;

by Th1;

:: original: \

redefine func X \ Y -> Element of A;

correctness

coherence

X \ Y is Element of A;

by Th1;

end;
let X, Y be Element of A;

:: original: \/

redefine func X \/ Y -> Element of A;

correctness

coherence

X \/ Y is Element of A;

by Th1;

:: original: \

redefine func X \ Y -> Element of A;

correctness

coherence

X \ Y is Element of A;

by Th1;

theorem Th2: :: FINSUB_1:2

for X, Y being set

for A being non empty preBoolean set st X is Element of A & Y is Element of A holds

X /\ Y is Element of A

for A being non empty preBoolean set st X is Element of A & Y is Element of A holds

X /\ Y is Element of A

proof end;

theorem Th3: :: FINSUB_1:3

for X, Y being set

for A being non empty preBoolean set st X is Element of A & Y is Element of A holds

X \+\ Y is Element of A

for A being non empty preBoolean set st X is Element of A & Y is Element of A holds

X \+\ Y is Element of A

proof end;

theorem :: FINSUB_1:4

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

( X \+\ Y in A & X \ Y in A ) ) holds

A is preBoolean

proof end;

theorem :: FINSUB_1:5

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

( X \+\ Y in A & X /\ Y in A ) ) holds

A is preBoolean

proof end;

theorem :: FINSUB_1:6

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

( X \+\ Y in A & X \/ Y in A ) ) holds

A is preBoolean

proof end;

definition

let A be non empty preBoolean set ;

let X, Y be Element of A;

:: original: /\

redefine func X /\ Y -> Element of A;

coherence

X /\ Y is Element of A by Th2;

:: original: \+\

redefine func X \+\ Y -> Element of A;

coherence

X \+\ Y is Element of A by Th3;

end;
let X, Y be Element of A;

:: original: /\

redefine func X /\ Y -> Element of A;

coherence

X /\ Y is Element of A by Th2;

:: original: \+\

redefine func X \+\ Y -> Element of A;

coherence

X \+\ Y is Element of A by Th3;

registration
end;

:: The set of all finite subsets of a set

definition

let A be set ;

ex b_{1} being preBoolean set st

for X being set holds

( X in b_{1} iff ( X c= A & X is finite ) )

for b_{1}, b_{2} being preBoolean set st ( for X being set holds

( X in b_{1} iff ( X c= A & X is finite ) ) ) & ( for X being set holds

( X in b_{2} iff ( X c= A & X is finite ) ) ) holds

b_{1} = b_{2}

end;
func Fin A -> preBoolean set means :Def5: :: FINSUB_1:def 5

for X being set holds

( X in it iff ( X c= A & X is finite ) );

existence for X being set holds

( X in it iff ( X c= A & X is finite ) );

ex b

for X being set holds

( X in b

proof end;

uniqueness for b

( X in b

( X in b

b

proof end;

:: deftheorem Def5 defines Fin FINSUB_1:def 5 :

for A being set

for b_{2} being preBoolean set holds

( b_{2} = Fin A iff for X being set holds

( X in b_{2} iff ( X c= A & X is finite ) ) );

for A being set

for b

( b

( X in b

registration
end;

registration
end;

:: Finite subsets

theorem :: FINSUB_1:17

theorem :: FINSUB_1:18