let S be 1-sorted ; :: thesis: for D being MSClosureSystem of S holds ClOp->ClSys (ClSys->ClOp D) = MSClosureStr(# the Sorts of D, the Family of D #)

let D be MSClosureSystem of S; :: thesis: ClOp->ClSys (ClSys->ClOp D) = MSClosureStr(# the Sorts of D, the Family of D #)

set M = the Sorts of D;

set F = the Family of D;

set I = the carrier of S;

consider X1 being ManySortedSet of the carrier of S such that

A1: X1 in bool the Sorts of D by PBOOLE:134;

the Family of D = MSFixPoints (ClSys->ClOp D)

let D be MSClosureSystem of S; :: thesis: ClOp->ClSys (ClSys->ClOp D) = MSClosureStr(# the Sorts of D, the Family of D #)

set M = the Sorts of D;

set F = the Family of D;

set I = the carrier of S;

consider X1 being ManySortedSet of the carrier of S such that

A1: X1 in bool the Sorts of D by PBOOLE:134;

the Family of D = MSFixPoints (ClSys->ClOp D)

proof

hence
ClOp->ClSys (ClSys->ClOp D) = MSClosureStr(# the Sorts of D, the Family of D #)
by Def13; :: thesis: verum
A2:
dom (ClSys->ClOp D) = the carrier of S
by PARTFUN1:def 2;

let i be object ; :: according to PBOOLE:def 10 :: thesis: ( not i in the carrier of S or the Family of D . i = (MSFixPoints (ClSys->ClOp D)) . i )

assume A3: i in the carrier of S ; :: thesis: the Family of D . i = (MSFixPoints (ClSys->ClOp D)) . i

reconsider f = (ClSys->ClOp D) . i as Function of ((bool the Sorts of D) . i),((bool the Sorts of D) . i) by A3, PBOOLE:def 15;

reconsider Fi = the Family of D . i as non empty set by A3;

thus the Family of D . i c= (MSFixPoints (ClSys->ClOp D)) . i :: according to XBOOLE_0:def 10 :: thesis: (MSFixPoints (ClSys->ClOp D)) . i c= the Family of D . i

assume A16: x in (MSFixPoints (ClSys->ClOp D)) . i ; :: thesis: x in the Family of D . i

then A17: ex f being Function st

( f = (ClSys->ClOp D) . i & x in dom f & f . x = x ) by A3, Def12;

dom (X1 +* (i .--> x)) = the carrier of S by A3, PZFMISC1:1;

then reconsider X = X1 +* (i .--> x) as ManySortedSet of the carrier of S by PARTFUN1:def 2, RELAT_1:def 18;

A18: dom (i .--> x) = {i} ;

i in {i} by TARSKI:def 1;

then A19: X . i = (i .--> x) . i by A18, FUNCT_4:13

.= x by FUNCOP_1:72 ;

MSFixPoints (ClSys->ClOp D) c= bool the Sorts of D by PBOOLE:def 18;

then A20: (MSFixPoints (ClSys->ClOp D)) . i c= (bool the Sorts of D) . i by A3;

X is Element of bool the Sorts of D

defpred S_{1}[ ManySortedSet of the carrier of S] means X c= $1;

consider SF being V8() MSSubsetFamily of the Sorts of D such that

A22: for Y being ManySortedSet of the carrier of S holds

( Y in SF iff ( Y in the Family of D & X c= Y ) ) by Th31;

A23: dom (ClSys->ClOp D) = the carrier of S by PARTFUN1:def 2;

( ( for Y being ManySortedSet of the carrier of S holds

( Y in SF iff ( Y in the Family of D & S_{1}[Y] ) ) ) implies SF c= the Family of D )
from CLOSURE1:sch 1();

then A24: meet SF in the Family of D by A22, MSSUBFAM:def 5;

(meet SF) . i = ((ClSys->ClOp D) .. X) . i by A22, Def14

.= x by A3, A17, A19, A23, PRALG_1:def 17 ;

hence x in the Family of D . i by A3, A24; :: thesis: verum

end;let i be object ; :: according to PBOOLE:def 10 :: thesis: ( not i in the carrier of S or the Family of D . i = (MSFixPoints (ClSys->ClOp D)) . i )

assume A3: i in the carrier of S ; :: thesis: the Family of D . i = (MSFixPoints (ClSys->ClOp D)) . i

reconsider f = (ClSys->ClOp D) . i as Function of ((bool the Sorts of D) . i),((bool the Sorts of D) . i) by A3, PBOOLE:def 15;

reconsider Fi = the Family of D . i as non empty set by A3;

thus the Family of D . i c= (MSFixPoints (ClSys->ClOp D)) . i :: according to XBOOLE_0:def 10 :: thesis: (MSFixPoints (ClSys->ClOp D)) . i c= the Family of D . i

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (MSFixPoints (ClSys->ClOp D)) . i or x in the Family of D . i )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the Family of D . i or x in (MSFixPoints (ClSys->ClOp D)) . i )

assume A4: x in the Family of D . i ; :: thesis: x in (MSFixPoints (ClSys->ClOp D)) . i

reconsider xx = x as set by TARSKI:1;

dom (X1 +* (i .--> x)) = the carrier of S by A3, PZFMISC1:1;

then reconsider X = X1 +* (i .--> x) as ManySortedSet of the carrier of S by PARTFUN1:def 2, RELAT_1:def 18;

A5: dom (i .--> x) = {i} ;

the Family of D c= bool the Sorts of D by PBOOLE:def 18;

then A6: the Family of D . i c= (bool the Sorts of D) . i by A3;

then x in (bool the Sorts of D) . i by A4;

then A7: x in dom f by FUNCT_2:def 1;

i in {i} by TARSKI:def 1;

then A8: X . i = (i .--> x) . i by A5, FUNCT_4:13

.= x by FUNCOP_1:72 ;

X is Element of bool the Sorts of D

consider SF being V8() MSSubsetFamily of the Sorts of D such that

A10: for Y being ManySortedSet of the carrier of S holds

( Y in SF iff ( Y in the Family of D & X c= Y ) ) by Th31;

consider Q being Subset-Family of ( the Sorts of D . i) such that

A11: Q = SF . i and

A12: (meet SF) . i = Intersect Q by A3, MSSUBFAM:def 1;

A13: SF . i = { z where z is Element of Fi : X . i c= z } by A3, A10, Th32;

x in { B where B is Element of Fi : xx c= B } by A4;

then Intersect Q c= xx by A8, A11, A13, MSSUBFAM:2;

then A15: Intersect Q = x by A14, XBOOLE_0:def 10;

(ClSys->ClOp D) .. X = meet SF by A10, Def14;

then f . x = x by A3, A8, A12, A15, A2, PRALG_1:def 17;

hence x in (MSFixPoints (ClSys->ClOp D)) . i by A3, A7, Def12; :: thesis: verum

end;assume A4: x in the Family of D . i ; :: thesis: x in (MSFixPoints (ClSys->ClOp D)) . i

reconsider xx = x as set by TARSKI:1;

dom (X1 +* (i .--> x)) = the carrier of S by A3, PZFMISC1:1;

then reconsider X = X1 +* (i .--> x) as ManySortedSet of the carrier of S by PARTFUN1:def 2, RELAT_1:def 18;

A5: dom (i .--> x) = {i} ;

the Family of D c= bool the Sorts of D by PBOOLE:def 18;

then A6: the Family of D . i c= (bool the Sorts of D) . i by A3;

then x in (bool the Sorts of D) . i by A4;

then A7: x in dom f by FUNCT_2:def 1;

i in {i} by TARSKI:def 1;

then A8: X . i = (i .--> x) . i by A5, FUNCT_4:13

.= x by FUNCOP_1:72 ;

X is Element of bool the Sorts of D

proof

then reconsider X = X as Element of bool the Sorts of D ;
let s be object ; :: according to PBOOLE:def 14 :: thesis: ( not s in the carrier of S or X . s is Element of (bool the Sorts of D) . s )

assume A9: s in the carrier of S ; :: thesis: X . s is Element of (bool the Sorts of D) . s

end;assume A9: s in the carrier of S ; :: thesis: X . s is Element of (bool the Sorts of D) . s

consider SF being V8() MSSubsetFamily of the Sorts of D such that

A10: for Y being ManySortedSet of the carrier of S holds

( Y in SF iff ( Y in the Family of D & X c= Y ) ) by Th31;

consider Q being Subset-Family of ( the Sorts of D . i) such that

A11: Q = SF . i and

A12: (meet SF) . i = Intersect Q by A3, MSSUBFAM:def 1;

A13: SF . i = { z where z is Element of Fi : X . i c= z } by A3, A10, Th32;

now :: thesis: for Z1 being set st Z1 in Q holds

xx c= Z1

then A14:
xx c= Intersect Q
by A3, A11, MSSUBFAM:5;xx c= Z1

let Z1 be set ; :: thesis: ( Z1 in Q implies xx c= Z1 )

assume Z1 in Q ; :: thesis: xx c= Z1

then ex q being Element of Fi st

( q = Z1 & X . i c= q ) by A11, A13;

hence xx c= Z1 by A8; :: thesis: verum

end;assume Z1 in Q ; :: thesis: xx c= Z1

then ex q being Element of Fi st

( q = Z1 & X . i c= q ) by A11, A13;

hence xx c= Z1 by A8; :: thesis: verum

x in { B where B is Element of Fi : xx c= B } by A4;

then Intersect Q c= xx by A8, A11, A13, MSSUBFAM:2;

then A15: Intersect Q = x by A14, XBOOLE_0:def 10;

(ClSys->ClOp D) .. X = meet SF by A10, Def14;

then f . x = x by A3, A8, A12, A15, A2, PRALG_1:def 17;

hence x in (MSFixPoints (ClSys->ClOp D)) . i by A3, A7, Def12; :: thesis: verum

assume A16: x in (MSFixPoints (ClSys->ClOp D)) . i ; :: thesis: x in the Family of D . i

then A17: ex f being Function st

( f = (ClSys->ClOp D) . i & x in dom f & f . x = x ) by A3, Def12;

dom (X1 +* (i .--> x)) = the carrier of S by A3, PZFMISC1:1;

then reconsider X = X1 +* (i .--> x) as ManySortedSet of the carrier of S by PARTFUN1:def 2, RELAT_1:def 18;

A18: dom (i .--> x) = {i} ;

i in {i} by TARSKI:def 1;

then A19: X . i = (i .--> x) . i by A18, FUNCT_4:13

.= x by FUNCOP_1:72 ;

MSFixPoints (ClSys->ClOp D) c= bool the Sorts of D by PBOOLE:def 18;

then A20: (MSFixPoints (ClSys->ClOp D)) . i c= (bool the Sorts of D) . i by A3;

X is Element of bool the Sorts of D

proof

then reconsider X = X as Element of bool the Sorts of D ;
let s be object ; :: according to PBOOLE:def 14 :: thesis: ( not s in the carrier of S or X . s is Element of (bool the Sorts of D) . s )

assume A21: s in the carrier of S ; :: thesis: X . s is Element of (bool the Sorts of D) . s

end;assume A21: s in the carrier of S ; :: thesis: X . s is Element of (bool the Sorts of D) . s

defpred S

consider SF being V8() MSSubsetFamily of the Sorts of D such that

A22: for Y being ManySortedSet of the carrier of S holds

( Y in SF iff ( Y in the Family of D & X c= Y ) ) by Th31;

A23: dom (ClSys->ClOp D) = the carrier of S by PARTFUN1:def 2;

( ( for Y being ManySortedSet of the carrier of S holds

( Y in SF iff ( Y in the Family of D & S

then A24: meet SF in the Family of D by A22, MSSUBFAM:def 5;

(meet SF) . i = ((ClSys->ClOp D) .. X) . i by A22, Def14

.= x by A3, A17, A19, A23, PRALG_1:def 17 ;

hence x in the Family of D . i by A3, A24; :: thesis: verum