begin
theorem
theorem
canceled;
theorem Th3:
begin
:: deftheorem Def1 defines Bool CLOSURE2:def 1 :
theorem Th4:
theorem
theorem
theorem
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem
theorem
begin
:: deftheorem CLOSURE2:def 2 :
canceled;
:: deftheorem Def3 defines |. CLOSURE2:def 3 :
theorem Th14:
:: deftheorem Def4 defines |: CLOSURE2:def 4 :
theorem Th15:
theorem Th16:
theorem
theorem Th18:
theorem
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem
:: deftheorem defines additive CLOSURE2:def 5 :
:: deftheorem Def6 defines absolutely-additive CLOSURE2:def 6 :
:: deftheorem defines multiplicative CLOSURE2:def 7 :
:: deftheorem Def8 defines absolutely-multiplicative CLOSURE2:def 8 :
:: deftheorem Def9 defines properly-upper-bound CLOSURE2:def 9 :
:: deftheorem Def10 defines properly-lower-bound CLOSURE2:def 10 :
Lm1:
for I being set
for M being ManySortedSet of I holds
( Bool M is additive & Bool M is absolutely-additive & Bool M is multiplicative & Bool M is absolutely-multiplicative & Bool M is properly-upper-bound & Bool M is properly-lower-bound )
begin
:: deftheorem CLOSURE2:def 11 :
canceled;
:: deftheorem Def12 defines reflexive CLOSURE2:def 12 :
:: deftheorem Def13 defines monotonic CLOSURE2:def 13 :
:: deftheorem Def14 defines idempotent CLOSURE2:def 14 :
:: deftheorem Def15 defines topological CLOSURE2:def 15 :
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
begin
:: deftheorem Def16 defines additive CLOSURE2:def 16 :
:: deftheorem Def17 defines absolutely-additive CLOSURE2:def 17 :
:: deftheorem Def18 defines multiplicative CLOSURE2:def 18 :
:: deftheorem Def19 defines absolutely-multiplicative CLOSURE2:def 19 :
:: deftheorem Def20 defines properly-upper-bound CLOSURE2:def 20 :
:: deftheorem Def21 defines properly-lower-bound CLOSURE2:def 21 :
:: deftheorem defines Full CLOSURE2:def 22 :
theorem Th39:
:: deftheorem Def23 defines ClOp->ClSys CLOSURE2:def 23 :
:: deftheorem Def24 defines Cl CLOSURE2:def 24 :
theorem Th40:
theorem
theorem Th42:
:: deftheorem Def25 defines ClSys->ClOp CLOSURE2:def 25 :
theorem
deffunc H1( set ) -> set = $1;
theorem