begin
theorem
theorem
:: deftheorem PBOOLE:def 1 :
canceled;
:: deftheorem PBOOLE:def 2 :
canceled;
:: deftheorem PBOOLE:def 3 :
canceled;
scheme
KuratowskiFunction{
F1()
-> set ,
F2(
set )
-> set } :
provided
A1:
for
e being
set st
e in F1() holds
F2(
e)
<> {}
:: deftheorem Def4 defines in PBOOLE:def 4 :
:: deftheorem Def5 defines c= PBOOLE:def 5 :
theorem Th3:
definition
let I be
set ;
func [0] I -> ManySortedSet of
I equals
I --> {} ;
coherence
I --> {} is ManySortedSet of I
correctness
;
let X,
Y be
ManySortedSet of
I;
func X \/ Y -> ManySortedSet of
I means :
Def7:
for
i being
set st
i in I holds
it . i = (X . i) \/ (Y . i);
existence
ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i = (X . i) \/ (Y . i)
uniqueness
for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = (X . i) \/ (Y . i) ) & ( for i being set st i in I holds
b2 . i = (X . i) \/ (Y . i) ) holds
b1 = b2
commutativity
for b1, X, Y being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = (X . i) \/ (Y . i) ) holds
for i being set st i in I holds
b1 . i = (Y . i) \/ (X . i)
;
idempotence
for X being ManySortedSet of I
for i being set st i in I holds
X . i = (X . i) \/ (X . i)
;
func X /\ Y -> ManySortedSet of
I means :
Def8:
for
i being
set st
i in I holds
it . i = (X . i) /\ (Y . i);
existence
ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i = (X . i) /\ (Y . i)
uniqueness
for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = (X . i) /\ (Y . i) ) & ( for i being set st i in I holds
b2 . i = (X . i) /\ (Y . i) ) holds
b1 = b2
commutativity
for b1, X, Y being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = (X . i) /\ (Y . i) ) holds
for i being set st i in I holds
b1 . i = (Y . i) /\ (X . i)
;
idempotence
for X being ManySortedSet of I
for i being set st i in I holds
X . i = (X . i) /\ (X . i)
;
func X \ Y -> ManySortedSet of
I means :
Def9:
for
i being
set st
i in I holds
it . i = (X . i) \ (Y . i);
existence
ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i = (X . i) \ (Y . i)
uniqueness
for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = (X . i) \ (Y . i) ) & ( for i being set st i in I holds
b2 . i = (X . i) \ (Y . i) ) holds
b1 = b2
pred X overlaps Y means :
Def10:
for
i being
set st
i in I holds
X . i meets Y . i;
symmetry
for X, Y being ManySortedSet of I st ( for i being set st i in I holds
X . i meets Y . i ) holds
for i being set st i in I holds
Y . i meets X . i
;
pred X misses Y means :
Def11:
for
i being
set st
i in I holds
X . i misses Y . i;
symmetry
for X, Y being ManySortedSet of I st ( for i being set st i in I holds
X . i misses Y . i ) holds
for i being set st i in I holds
Y . i misses X . i
;
end;
:: deftheorem defines [0] PBOOLE:def 6 :
:: deftheorem Def7 defines \/ PBOOLE:def 7 :
:: deftheorem Def8 defines /\ PBOOLE:def 8 :
:: deftheorem Def9 defines \ PBOOLE:def 9 :
:: deftheorem Def10 defines overlaps PBOOLE:def 10 :
:: deftheorem Def11 defines misses PBOOLE:def 11 :
:: deftheorem defines \+\ PBOOLE:def 12 :
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem
begin
:: deftheorem Def13 defines = PBOOLE:def 13 :
theorem
canceled;
theorem
canceled;
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem
theorem Th21:
theorem Th22:
theorem
theorem Th24:
theorem Th25:
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
begin
theorem Th49:
theorem Th50:
theorem
theorem
theorem Th53:
theorem
theorem
theorem
theorem
begin
theorem Th58:
theorem Th59:
theorem Th60:
theorem
theorem Th62:
theorem
theorem
theorem Th65:
theorem Th66:
theorem
theorem Th68:
theorem Th69:
theorem Th70:
theorem Th71:
theorem
theorem Th73:
theorem Th74:
theorem Th75:
theorem Th76:
theorem
theorem Th78:
theorem Th79:
theorem
theorem Th81:
theorem
theorem Th83:
theorem Th84:
theorem
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
theorem
theorem
canceled;
theorem
theorem Th95:
theorem
theorem
theorem Th98:
theorem
theorem Th100:
theorem Th101:
theorem Th102:
theorem Th103:
theorem
theorem
begin
theorem
theorem
canceled;
theorem Th108:
theorem Th109:
theorem Th110:
theorem
theorem
theorem
theorem
theorem
theorem Th116:
theorem
canceled;
theorem Th118:
theorem
theorem
theorem Th121:
theorem
theorem
theorem
theorem
canceled;
theorem Th126:
theorem
theorem
theorem
begin
:: deftheorem Def14 defines [= PBOOLE:def 14 :
theorem
theorem
canceled;
theorem
begin
theorem
theorem
theorem
theorem Th136:
theorem
theorem
theorem Th139:
theorem
begin
:: deftheorem Def15 defines empty-yielding PBOOLE:def 15 :
:: deftheorem Def16 defines non-empty PBOOLE:def 16 :
theorem
theorem
theorem Th143:
theorem Th144:
theorem
theorem
theorem Th147:
theorem
begin
scheme
MSSEx{
F1()
-> set ,
P1[
set ,
set ] } :
provided
A1:
for
i being
set st
i in F1() holds
ex
j being
set st
P1[
i,
j]
begin
theorem Th149:
theorem
theorem
:: deftheorem defines Element PBOOLE:def 17 :
begin
:: deftheorem Def18 defines ManySortedFunction PBOOLE:def 18 :
:: deftheorem Def19 defines # PBOOLE:def 19 :
:: deftheorem Def20 defines *--> PBOOLE:def 20 :
theorem Th152:
theorem
:: deftheorem defines [| PBOOLE:def 21 :
:: deftheorem defines MSFuncs PBOOLE:def 22 :
:: deftheorem Def23 defines ManySortedSubset PBOOLE:def 23 :
:: deftheorem Def24 defines ** PBOOLE:def 24 :
:: deftheorem defines .:.: PBOOLE:def 25 :
theorem
theorem
theorem