:: CLOSURE1 semantic presentation

scheme :: CLOSURE1:sch 1
s1{ F₁() -> set , F₂() -> V3 ManySortedSet of F₁(), F₃() -> ManySortedSet of F₁(), P₁[ set ] } :

( ( for b₁ being ManySortedSet of F₁() holds
( b₁ in F₂() iff ( b₁ in F₃() & P₁[b₁] ) ) ) implies F₂() c= F₃() )

proof end;

theorem Th1: :: CLOSURE1:1

for b₁ being non empty set
for b₂, b₃ being set st b₂ c= b₃ holds
{ b₄ where B is Element of b₁ : b₃ c= b₄ } c= { b₄ where B is Element of b₁ : b₂ c= b₄ }

proof end;

theorem Th2: :: CLOSURE1:2

for b₁ being set
for b₂ being ManySortedSet of b₁ st ex b₃ being ManySortedSet of b₁ st b₃ in b₂ holds
b₂ is non-empty

proof end;

definition

let c₁ be set ;
let c₂ be ManySortedFunction of c₁;
let c₃ be ManySortedSet of c₁;
redefine func .. as c₂ .. c₃ -> ManySortedSet of a₁;
coherence

proof end;

end;

E2: now

let c₁ be set ;
let c₂, c₃ be V3 ManySortedSet of c₁;
let c₄ be ManySortedFunction of c₂,c₃;
let c₅ be Element of c₂;
thus c₄ .. c₅ is Element of c₃

proof

let c₆ be set ; :: according to PBOOLE:def 17
assume E3: c₆ in c₁ ;
E4: dom c₄ = c₁ by PBOOLE:def 3;
reconsider c₇ = c₄ . c₆ as Function ;
E5: c₇ is Function of c₂ . c₆,c₃ . c₆ by E3, PBOOLE:def 18;
E6: c₂ . c₆ <> {} by E3, PBOOLE:def 16;
E7: c₃ . c₆ <> {} by E3, PBOOLE:def 16;
c₅ . c₆ is Element of c₂ . c₆ by E3, PBOOLE:def 17;
then c₇ . (c₅ . c₆) in c₃ . c₆ by E5, E6, E7, FUNCT_2:7;
hence (c₄ .. c₅) . c₆ is Element of c₃ . c₆ by E3, E4, PRALG_1:def 17;

end;

definition

let c₁ be set ;
let c₂, c₃ be V3 ManySortedSet of c₁;
let c₄ be ManySortedFunction of c₂,c₃;
let c₅ be Element of c₂;
redefine func .. as c₄ .. c₅ -> Element of a₃;
coherence by Lemma2;

end;

theorem Th3: :: CLOSURE1:3

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁
for b₄ being V3 ManySortedSet of b₁
for b₅ being ManySortedFunction of b₂,b₄ st b₃ in b₂ holds
b₅ .. b₃ in b₄

proof end;

theorem Th4: :: CLOSURE1:4

for b₁ being set
for b₂, b₃ being ManySortedFunction of b₁
for b₄ being ManySortedSet of b₁ st b₄ in doms b₃ holds
b₂ .. (b₃ .. b₄) = (b₂ ** b₃) .. b₄

proof end;

theorem Th5: :: CLOSURE1:5

for b₁ being set
for b₂ being ManySortedFunction of b₁ st b₂ is "1-1" holds
for b₃, b₄ being ManySortedSet of b₁ st b₃ in doms b₂ & b₄ in doms b₂ & b₂ .. b₃ = b₂ .. b₄ holds
b₃ = b₄

proof end;

theorem Th6: :: CLOSURE1:6

for b₁ being set
for b₂ being ManySortedFunction of b₁ st doms b₂ is non-empty & ( for b₃, b₄ being ManySortedSet of b₁ st b₃ in doms b₂ & b₄ in doms b₂ & b₂ .. b₃ = b₂ .. b₄ holds
b₃ = b₄ ) holds
b₂ is "1-1"

proof end;

theorem Th7: :: CLOSURE1:7

for b₁ being set
for b₂, b₃ being V3 ManySortedSet of b₁
for b₄, b₅ being ManySortedFunction of b₂,b₃ st ( for b₆ being ManySortedSet of b₁ st b₆ in b₂ holds
b₄ .. b₆ = b₅ .. b₆ ) holds
b₄ = b₅

proof end;

registration

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
cluster V4 locally-finite Element of bool a₂;
existence

proof end;

end;

definition

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
mode MSSetOp of a₂ is ManySortedFunction of bool a₂, bool a₂;

end;

definition

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
let c₃ be MSSetOp of c₂;
let c₄ be Element of bool c₂;
redefine func .. as c₃ .. c₄ -> Element of bool a₂;
coherence by Lemma2;

end;

definition

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
let c₃ be MSSetOp of c₂;
canceled;
attr a₃ is reflexive means :Def2: :: CLOSURE1:def 2
for b₁ being Element of bool a₂ holds b₁ c= a₃ .. b₁;
attr a₃ is monotonic means :Def3: :: CLOSURE1:def 3
for b₁, b₂ being Element of bool a₂ st b₁ c= b₂ holds
a₃ .. b₁ c= a₃ .. b₂;
attr a₃ is idempotent means :Def4: :: CLOSURE1:def 4
for b₁ being Element of bool a₂ holds a₃ .. b₁ = a₃ .. (a₃ .. b₁);
attr a₃ is topological means :Def5: :: CLOSURE1:def 5
for b₁, b₂ being Element of bool a₂ holds a₃ .. (b₁ \/ b₂) = (a₃ .. b₁) \/ (a₃ .. b₂);

end;

:: deftheorem Def1 CLOSURE1:def 1 :

:: 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: :: CLOSURE1:8

for b₁ being set
for b₂ being V3 ManySortedSet of b₁
for b₃ being Element of b₂ holds b₃ = (id b₂) .. b₃

proof end;

theorem Th9: :: CLOSURE1:9

for b₁ being set
for b₂ being V3 ManySortedSet of b₁
for b₃, b₄ being Element of b₂ st b₃ c= b₄ holds
(id b₂) .. b₃ c= (id b₂) .. b₄

proof end;

theorem Th10: :: CLOSURE1:10

for b₁ being set
for b₂ being V3 ManySortedSet of b₁
for b₃, b₄ being Element of b₂ st b₃ \/ b₄ is Element of b₂ holds
(id b₂) .. (b₃ \/ b₄) = ((id b₂) .. b₃) \/ ((id b₂) .. b₄)

proof end;

theorem Th11: :: CLOSURE1:11

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃ being Element of bool b₂
for b₄, b₅ being set st b₄ in b₁ & b₅ in ((id (bool b₂)) .. b₃) . b₄ holds
ex b₆ being locally-finite Element of bool b₂ st
( b₆ c= b₃ & b₅ in ((id (bool b₂)) .. b₆) . b₄ )

proof end;

registration

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
cluster reflexive monotonic idempotent topological ManySortedFunction of bool a₂, bool a₂;
existence

proof end;

end;

theorem Th12: :: CLOSURE1:12

for b₁ being set
for b₂ being ManySortedSet of b₁ holds id (bool b₂) is reflexive MSSetOp of b₂

proof end;

theorem Th13: :: CLOSURE1:13

for b₁ being set
for b₂ being ManySortedSet of b₁ holds id (bool b₂) is monotonic MSSetOp of b₂

proof end;

theorem Th14: :: CLOSURE1:14

for b₁ being set
for b₂ being ManySortedSet of b₁ holds id (bool b₂) is idempotent MSSetOp of b₂

proof end;

theorem Th15: :: CLOSURE1:15

for b₁ being set
for b₂ being ManySortedSet of b₁ holds id (bool b₂) is topological MSSetOp of b₂

proof end;

theorem Th16: :: CLOSURE1:16

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃ being MSSetOp of b₂
for b₄ being Element of bool b₂ st b₄ = b₂ & b₃ is reflexive holds
b₄ = b₃ .. b₄

proof end;

theorem Th17: :: CLOSURE1:17

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃ being MSSetOp of b₂ st b₃ is reflexive & ( for b₄ being Element of bool b₂ holds b₃ .. b₄ c= b₄ ) holds
b₃ is idempotent

proof end;

theorem Th18: :: CLOSURE1:18

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃ being MSSetOp of b₂
for b₄, b₅ being Element of bool b₂ st b₃ is monotonic holds
b₃ .. (b₄ /\ b₅) c= (b₃ .. b₄) /\ (b₃ .. b₅)

proof end;

registration

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
cluster topological -> monotonic ManySortedFunction of bool a₂, bool a₂;
coherence

proof end;

end;

theorem Th19: :: CLOSURE1:19

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃ being MSSetOp of b₂
for b₄, b₅ being Element of bool b₂ st b₃ is topological holds
(b₃ .. b₄) \ (b₃ .. b₅) c= b₃ .. (b₄ \ b₅)

proof end;

definition

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
let c₃, c₄ be MSSetOp of c₂;
redefine func ** as c₄ ** c₃ -> MSSetOp of a₂;
coherence

proof end;

end;

theorem Th20: :: CLOSURE1:20

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃, b₄ being MSSetOp of b₂ st b₃ is reflexive & b₄ is reflexive holds
b₃ ** b₄ is reflexive

proof end;

theorem Th21: :: CLOSURE1:21

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃, b₄ being MSSetOp of b₂ st b₃ is monotonic & b₄ is monotonic holds
b₃ ** b₄ is monotonic

proof end;

theorem Th22: :: CLOSURE1:22

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃, b₄ being MSSetOp of b₂ st b₃ is idempotent & b₄ is idempotent & b₃ ** b₄ = b₄ ** b₃ holds
b₃ ** b₄ is idempotent

proof end;

theorem Th23: :: CLOSURE1:23

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃, b₄ being MSSetOp of b₂ st b₃ is topological & b₄ is topological holds
b₃ ** b₄ is topological

proof end;

E12: now

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
let c₃ be set ;
let c₄ be ManySortedSet of c₁;
let c₅ be Element of bool (c₂ . c₃);
assume that
c₃ in c₁ and
E13: c₄ = ([0] c₁) +* (c₃ .--> c₅) ;
[0] c₁ c= c₂ by MBOOLEAN:5;
then E14: [0] c₁ in bool c₂ by MBOOLEAN:1;
E15: dom (c₃ .--> c₅) = {c₃} by CQC_LANG:5;
thus c₄ in bool c₂

proof

let c₆ be set ; :: according to PBOOLE:def 4
assume E16: c₆ in c₁ ;
c₃ in {c₃} by TARSKI:def 1;
then E17: c₄ . c₃ = (c₃ .--> c₅) . c₃ by E13, E15, FUNCT_4:14
.= c₅ by CQC_LANG:6 ;

now

per cases ;

case E18: c₆ = c₃ ;

then c₅ in bool (c₂ . c₆) ;
hence c₄ . c₆ in (bool c₂) . c₆ by E16, E17, E18, MBOOLEAN:def 1;

end;

case c₆ <> c₃ ;

then not c₆ in dom (c₃ .--> c₅) by E15, TARSKI:def 1;
then c₄ . c₆ = ([0] c₁) . c₆ by E13, FUNCT_4:12;
hence c₄ . c₆ in (bool c₂) . c₆ by E14, E16, PBOOLE:def 4;

end;

hence c₄ . c₆ in (bool c₂) . c₆ ;

end;

theorem Th24: :: CLOSURE1:24

for b₁, b₂ being set
for b₃ being ManySortedSet of b₂
for b₄ being Function
for b₅ being MSSetOp of b₃ st b₅ is reflexive & b₁ in b₂ & b₄ = b₅ . b₁ holds
for b₆ being Element of bool (b₃ . b₁) holds b₆ c= b₄ . b₆

proof end;

theorem Th25: :: CLOSURE1:25

for b₁, b₂ being set
for b₃ being ManySortedSet of b₂
for b₄ being Function
for b₅ being MSSetOp of b₃ st b₅ is monotonic & b₁ in b₂ & b₄ = b₅ . b₁ holds
for b₆, b₇ being Element of bool (b₃ . b₁) st b₆ c= b₇ holds
b₄ . b₆ c= b₄ . b₇

proof end;

theorem Th26: :: CLOSURE1:26

for b₁, b₂ being set
for b₃ being ManySortedSet of b₂
for b₄ being Function
for b₅ being MSSetOp of b₃ st b₅ is idempotent & b₁ in b₂ & b₄ = b₅ . b₁ holds
for b₆ being Element of bool (b₃ . b₁) holds b₄ . b₆ = b₄ . (b₄ . b₆)

proof end;

theorem Th27: :: CLOSURE1:27

for b₁, b₂ being set
for b₃ being ManySortedSet of b₂
for b₄ being Function
for b₅ being MSSetOp of b₃ st b₅ is topological & b₁ in b₂ & b₄ = b₅ . b₁ holds
for b₆, b₇ being Element of bool (b₃ . b₁) holds b₄ . (b₆ \/ b₇) = (b₄ . b₆) \/ (b₄ . b₇)

proof end;

definition

let c₁ be 1-sorted ;
attr a₂ is strict;
struct MSClosureStr of c₁ -> many-sorted of a₁;
aggr MSClosureStr(# Sorts, Family #) -> MSClosureStr of a₁;
sel Family c₂ -> MSSubsetFamily of the Sorts of a₂;

end;

definition

let c₁ be 1-sorted ;
let c₂ be MSClosureStr of c₁;
attr a₂ is additive means :Def6: :: CLOSURE1:def 6
the Family of a₂ is additive;
attr a₂ is absolutely-additive means :Def7: :: CLOSURE1:def 7
the Family of a₂ is absolutely-additive;
attr a₂ is multiplicative means :Def8: :: CLOSURE1:def 8
the Family of a₂ is multiplicative;
attr a₂ is absolutely-multiplicative means :Def9: :: CLOSURE1:def 9
the Family of a₂ is absolutely-multiplicative;
attr a₂ is properly-upper-bound means :Def10: :: CLOSURE1:def 10
the Family of a₂ is properly-upper-bound;
attr a₂ is properly-lower-bound means :Def11: :: CLOSURE1:def 11
the Family of a₂ is properly-lower-bound;

end;

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

definition

let c₁ be 1-sorted ;
let c₂ be many-sorted of c₁;
func MSFull c₂ -> MSClosureStr of a₁ equals :: CLOSURE1:def 12
MSClosureStr(# the Sorts of a₂,(bool the Sorts of a₂) #);
correctness ;

end;

:: deftheorem Def12 defines MSFull CLOSURE1:def 12 :

registration

let c₁ be 1-sorted ;
let c₂ be many-sorted of c₁;
cluster MSFull a₂ -> strict additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ;
coherence

proof end;

end;

registration

let c₁ be 1-sorted ;
let c₂ be non-empty many-sorted of c₁;
cluster MSFull a₂ -> non-empty strict additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ;
coherence by MSUALG_1:def 8;

end;

registration

let c₁ be 1-sorted ;
cluster non-empty strict additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound MSClosureStr of a₁;
existence

proof end;

end;

registration

let c₁ be 1-sorted ;
let c₂ be additive MSClosureStr of c₁;
cluster the Family of a₂ -> additive ;
coherence by Def6;

end;

registration

let c₁ be 1-sorted ;
let c₂ be absolutely-additive MSClosureStr of c₁;
cluster the Family of a₂ -> absolutely-additive ;
coherence by Def7;

end;

registration

let c₁ be 1-sorted ;
let c₂ be multiplicative MSClosureStr of c₁;
cluster the Family of a₂ -> multiplicative ;
coherence by Def8;

end;

registration

let c₁ be 1-sorted ;
let c₂ be absolutely-multiplicative MSClosureStr of c₁;
cluster the Family of a₂ -> absolutely-multiplicative ;
coherence by Def9;

end;

registration

let c₁ be 1-sorted ;
let c₂ be properly-upper-bound MSClosureStr of c₁;
cluster the Family of a₂ -> properly-upper-bound ;
coherence by Def10;

end;

registration

let c₁ be 1-sorted ;
let c₂ be properly-lower-bound MSClosureStr of c₁;
cluster the Family of a₂ -> properly-lower-bound ;
coherence by Def11;

end;

registration

let c₁ be 1-sorted ;
let c₂ be V3 ManySortedSet of the carrier of c₁;
let c₃ be MSSubsetFamily of c₂;
cluster MSClosureStr(# a₂,a₃ #) -> non-empty ;
coherence

proof end;

end;

registration

let c₁ be 1-sorted ;
let c₂ be many-sorted of c₁;
let c₃ be additive MSSubsetFamily of the Sorts of c₂;
cluster MSClosureStr(# the Sorts of a₂,a₃ #) -> additive ;
coherence by Def6;

end;

registration

let c₁ be 1-sorted ;
let c₂ be many-sorted of c₁;
let c₃ be absolutely-additive MSSubsetFamily of the Sorts of c₂;
cluster MSClosureStr(# the Sorts of a₂,a₃ #) -> additive absolutely-additive ;
coherence by Def7;

end;

registration

let c₁ be 1-sorted ;
let c₂ be many-sorted of c₁;
let c₃ be multiplicative MSSubsetFamily of the Sorts of c₂;
cluster MSClosureStr(# the Sorts of a₂,a₃ #) -> multiplicative ;
coherence by Def8;

end;

registration

let c₁ be 1-sorted ;
let c₂ be many-sorted of c₁;
let c₃ be absolutely-multiplicative MSSubsetFamily of the Sorts of c₂;
cluster MSClosureStr(# the Sorts of a₂,a₃ #) -> multiplicative absolutely-multiplicative ;
coherence by Def9;

end;

registration

let c₁ be 1-sorted ;
let c₂ be many-sorted of c₁;
let c₃ be properly-upper-bound MSSubsetFamily of the Sorts of c₂;
cluster MSClosureStr(# the Sorts of a₂,a₃ #) -> properly-upper-bound ;
coherence by Def10;

end;

registration

let c₁ be 1-sorted ;
let c₂ be many-sorted of c₁;
let c₃ be properly-lower-bound MSSubsetFamily of the Sorts of c₂;
cluster MSClosureStr(# the Sorts of a₂,a₃ #) -> properly-lower-bound ;
coherence by Def11;

end;

registration

let c₁ be 1-sorted ;
cluster absolutely-additive -> additive MSClosureStr of a₁;
coherence

proof end;

end;

registration

let c₁ be 1-sorted ;
cluster absolutely-multiplicative -> multiplicative MSClosureStr of a₁;
coherence

proof end;

end;

registration

let c₁ be 1-sorted ;
cluster absolutely-multiplicative -> properly-upper-bound MSClosureStr of a₁;
coherence

proof end;

end;

registration

let c₁ be 1-sorted ;
cluster absolutely-additive -> properly-lower-bound MSClosureStr of a₁;
coherence

proof end;

end;

definition

let c₁ be 1-sorted ;
mode MSClosureSystem of a₁ is absolutely-multiplicative MSClosureStr of a₁;

end;

definition

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
mode MSClosureOperator of a₂ is reflexive monotonic idempotent MSSetOp of a₂;

end;

definition

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
let c₃ be ManySortedFunction of c₂,c₂;
func MSFixPoints c₃ -> ManySortedSubset of a₂ means :Def13: :: CLOSURE1:def 13
for b₁, b₂ being set st b₂ in a₁ holds
( b₁ in a₄ . b₂ iff ex b₃ being Function st
( b₃ = a₃ . b₂ & b₁ in dom b₃ & b₃ . b₁ = b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines MSFixPoints CLOSURE1:def 13 :

registration

let c₁ be set ;
let c₂ be V4 ManySortedSet of c₁;
let c₃ be ManySortedFunction of c₂,c₂;
cluster MSFixPoints a₃ -> V4 ;
coherence

proof end;

end;

theorem Th28: :: CLOSURE1:28

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁
for b₄ being ManySortedFunction of b₂,b₂ holds
( ( b₃ in b₂ & b₄ .. b₃ = b₃ ) iff b₃ in MSFixPoints b₄ )

proof end;

theorem Th29: :: CLOSURE1:29

for b₁ being set
for b₂ being ManySortedSet of b₁ holds MSFixPoints (id b₂) = b₂

proof end;

theorem Th30: :: CLOSURE1:30

for b₁ being 1-sorted
for b₂ being ManySortedSet of the carrier of b₁
for b₃ being reflexive monotonic MSSetOp of b₂
for b₄ being MSSubsetFamily of b₂ st b₄ = MSFixPoints b₃ holds
MSClosureStr(# b₂,b₄ #) is MSClosureSystem of b₁

proof end;

theorem Th31: :: CLOSURE1:31

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃ being properly-upper-bound MSSubsetFamily of b₂
for b₄ being Element of bool b₂ ex b₅ being V3 MSSubsetFamily of b₂ st
for b₆ being ManySortedSet of b₁ holds
( b₆ in b₅ iff ( b₆ in b₃ & b₄ c= b₆ ) )

proof end;

theorem Th32: :: CLOSURE1:32

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃ being properly-upper-bound MSSubsetFamily of b₂
for b₄ being Element of bool b₂
for b₅ being V3 MSSubsetFamily of b₂ st ( for b₆ being ManySortedSet of b₁ holds
( b₆ in b₅ iff ( b₆ in b₃ & b₄ c= b₆ ) ) ) holds
for b₆ being set
for b₇ being non empty set st b₆ in b₁ & b₇ = b₃ . b₆ holds
b₅ . b₆ = { b₈ where B is Element of b₇ : b₄ . b₆ c= b₈ }

proof end;

theorem Th33: :: CLOSURE1:33

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃ being properly-upper-bound MSSubsetFamily of b₂ ex b₄ being MSSetOp of b₂ st
for b₅ being Element of bool b₂
for b₆ being V3 MSSubsetFamily of b₂ st ( for b₇ being ManySortedSet of b₁ holds
( b₇ in b₆ iff ( b₇ in b₃ & b₅ c= b₇ ) ) ) holds
b₄ .. b₅ = meet b₆

proof end;

theorem Th34: :: CLOSURE1:34

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃ being properly-upper-bound MSSubsetFamily of b₂
for b₄ being Element of bool b₂
for b₅ being MSSetOp of b₂ st b₄ in b₃ & ( for b₆ being Element of bool b₂
for b₇ being V3 MSSubsetFamily of b₂ st ( for b₈ being ManySortedSet of b₁ holds
( b₈ in b₇ iff ( b₈ in b₃ & b₆ c= b₈ ) ) ) holds
b₅ .. b₆ = meet b₇ ) holds
b₅ .. b₄ = b₄

proof end;

theorem Th35: :: CLOSURE1:35

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃ being absolutely-multiplicative MSSubsetFamily of b₂
for b₄ being Element of bool b₂
for b₅ being MSSetOp of b₂ st b₅ .. b₄ = b₄ & ( for b₆ being Element of bool b₂
for b₇ being V3 MSSubsetFamily of b₂ st ( for b₈ being ManySortedSet of b₁ holds
( b₈ in b₇ iff ( b₈ in b₃ & b₆ c= b₈ ) ) ) holds
b₅ .. b₆ = meet b₇ ) holds
b₄ in b₃

proof end;

theorem Th36: :: CLOSURE1:36

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃ being properly-upper-bound MSSubsetFamily of b₂
for b₄ being MSSetOp of b₂ st ( for b₅ being Element of bool b₂
for b₆ being V3 MSSubsetFamily of b₂ st ( for b₇ being ManySortedSet of b₁ holds
( b₇ in b₆ iff ( b₇ in b₃ & b₅ c= b₇ ) ) ) holds
b₄ .. b₅ = meet b₆ ) holds
( b₄ is reflexive & b₄ is monotonic )

proof end;

theorem Th37: :: CLOSURE1:37

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃ being absolutely-multiplicative MSSubsetFamily of b₂
for b₄ being MSSetOp of b₂ st ( for b₅ being Element of bool b₂
for b₆ being V3 MSSubsetFamily of b₂ st ( for b₇ being ManySortedSet of b₁ holds
( b₇ in b₆ iff ( b₇ in b₃ & b₅ c= b₇ ) ) ) holds
b₄ .. b₅ = meet b₆ ) holds
b₄ is idempotent

proof end;

theorem Th38: :: CLOSURE1:38

for b₁ being 1-sorted
for b₂ being MSClosureSystem of b₁
for b₃ being MSSetOp of the Sorts of b₂ st ( for b₄ being Element of bool the Sorts of b₂
for b₅ being V3 MSSubsetFamily of the Sorts of b₂ st ( for b₆ being ManySortedSet of the carrier of b₁ holds
( b₆ in b₅ iff ( b₆ in the Family of b₂ & b₄ c= b₆ ) ) ) holds
b₃ .. b₄ = meet b₅ ) holds
b₃ is MSClosureOperator of the Sorts of b₂ by Th36, Th37;

definition

let c₁ be 1-sorted ;
let c₂ be ManySortedSet of the carrier of c₁;
let c₃ be MSClosureOperator of c₂;
func ClOp->ClSys c₃ -> MSClosureSystem of a₁ means :Def14: :: CLOSURE1:def 14
ex b₁ being MSSubsetFamily of a₂ st
( b₁ = MSFixPoints a₃ & a₄ = MSClosureStr(# a₂,b₁ #) );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def14 defines ClOp->ClSys CLOSURE1:def 14 :

registration

let c₁ be 1-sorted ;
let c₂ be ManySortedSet of the carrier of c₁;
let c₃ be MSClosureOperator of c₂;
cluster ClOp->ClSys a₃ -> strict ;
coherence

proof end;

end;

registration

let c₁ be 1-sorted ;
let c₂ be V3 ManySortedSet of the carrier of c₁;
let c₃ be MSClosureOperator of c₂;
cluster ClOp->ClSys a₃ -> non-empty strict ;
coherence

proof end;

end;

definition

let c₁ be 1-sorted ;
let c₂ be MSClosureSystem of c₁;
func ClSys->ClOp c₂ -> MSClosureOperator of the Sorts of a₂ means :Def15: :: CLOSURE1:def 15
for b₁ being Element of bool the Sorts of a₂
for b₂ being V3 MSSubsetFamily of the Sorts of a₂ st ( for b₃ being ManySortedSet of the carrier of a₁ holds
( b₃ in b₂ iff ( b₃ in the Family of a₂ & b₁ c= b₃ ) ) ) holds
a₃ .. b₁ = meet b₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines ClSys->ClOp CLOSURE1:def 15 :

theorem Th39: :: CLOSURE1:39

for b₁ being 1-sorted
for b₂ being ManySortedSet of the carrier of b₁
for b₃ being MSClosureOperator of b₂ holds ClSys->ClOp (ClOp->ClSys b₃) = b₃

proof end;

theorem Th40: :: CLOSURE1:40

for b₁ being 1-sorted
for b₂ being MSClosureSystem of b₁ holds ClOp->ClSys (ClSys->ClOp b₂) = MSClosureStr(# the Sorts of b₂,the Family of b₂ #)

proof end;