begin
theorem Th1:
theorem
theorem
theorem Th4:
theorem
theorem
theorem Th7:
begin
:: deftheorem CLOSURE1:def 1 :
canceled;
:: deftheorem Def2 defines reflexive CLOSURE1:def 2 :
:: deftheorem Def3 defines monotonic CLOSURE1:def 3 :
:: deftheorem Def4 defines idempotent CLOSURE1:def 4 :
:: deftheorem Def5 defines topological CLOSURE1:def 5 :
theorem Th8:
theorem Th9:
theorem Th10:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th24:
theorem Th25:
theorem Th26:
theorem
begin
:: deftheorem Def6 defines additive CLOSURE1:def 6 :
:: deftheorem Def7 defines absolutely-additive CLOSURE1:def 7 :
:: deftheorem Def8 defines multiplicative CLOSURE1:def 8 :
:: deftheorem Def9 defines absolutely-multiplicative CLOSURE1:def 9 :
:: deftheorem Def10 defines properly-upper-bound CLOSURE1:def 10 :
:: deftheorem Def11 defines properly-lower-bound CLOSURE1:def 11 :
:: deftheorem defines MSFull CLOSURE1:def 12 :
:: deftheorem Def13 defines MSFixPoints CLOSURE1:def 13 :
theorem Th28:
theorem
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem
theorem Th36:
theorem Th37:
theorem
:: deftheorem Def14 defines ClOp->ClSys CLOSURE1:def 14 :
:: deftheorem Def15 defines ClSys->ClOp CLOSURE1:def 15 :
theorem
theorem