let S be 1-sorted ; :: thesis: for A being ManySortedSet of the carrier of S
for J being MSClosureOperator of A holds ClSys->ClOp () = J

let A be ManySortedSet of the carrier of S; :: thesis: for J being MSClosureOperator of A holds ClSys->ClOp () = J
let J be MSClosureOperator of A; :: thesis:
set I = the carrier of S;
set M = the Sorts of ();
set j = ClSys->ClOp ();
A1: ex D being MSSubsetFamily of A st
( D = MSFixPoints J & ClOp->ClSys J = MSClosureStr(# A,D #) ) by Def13;
for X being ManySortedSet of the carrier of S st X in bool A holds
() .. X = J .. X
proof
let X be ManySortedSet of the carrier of S; :: thesis: ( X in bool A implies () .. X = J .. X )
assume X in bool A ; :: thesis: () .. X = J .. X
then A2: X is Element of bool the Sorts of () by ;
then consider SF being V8() MSSubsetFamily of the Sorts of () such that
A3: for Y being ManySortedSet of the carrier of S holds
( Y in SF iff ( Y in MSFixPoints J & X c= Y ) ) by ;
now :: thesis: for i being object st i in the carrier of S holds
(() .. X) . i = (J .. X) . i
A4: dom J = the carrier of S by PARTFUN1:def 2;
let i be object ; :: thesis: ( i in the carrier of S implies (() .. X) . i = (J .. X) . i )
assume A5: i in the carrier of S ; :: thesis: (() .. X) . i = (J .. X) . i
reconsider f = J . i as Function of ((bool A) . i),((bool A) . i) by ;
(bool A) . i = bool (A . i) by ;
then reconsider f = f as Function of (bool (A . i)),(bool (A . i)) ;
X . i is Element of (bool A) . i by ;
then A6: X . i is Element of bool (A . i) by ;
then A7: X . i c= f . (X . i) by ;
reconsider Di = () . i as non empty set by A1, A5;
consider Q being Subset-Family of ( the Sorts of () . i) such that
A8: Q = SF . i and
A9: (meet SF) . i = Intersect Q by ;
A10: SF . i = { z where z is Element of Di : X . i c= z } by A1, A2, A3, A5, Th32;
now :: thesis: for x being set st x in Q holds
f . (X . i) c= x
let x be set ; :: thesis: ( x in Q implies f . (X . i) c= x )
assume x in Q ; :: thesis: f . (X . i) c= x
then consider x1 being Element of Di such that
A11: ( x1 = x & X . i c= x1 ) by ;
MSFixPoints J c= bool A by PBOOLE:def 18;
then Di c= (bool A) . i by A5;
then Di c= bool (A . i) by ;
then A12: x1 is Element of bool (A . i) ;
ex g being Function st
( g = J . i & x1 in dom g & g . x1 = x1 ) by ;
hence f . (X . i) c= x by A5, A6, A11, A12, Th25; :: thesis: verum
end;
then A13: f . (X . i) c= Intersect Q by ;
A14: ( dom f = bool (A . i) & f . (X . i) in bool (A . i) ) by ;
f . (f . (X . i)) = f . (X . i) by A5, A6, Th26;
then f . (X . i) is Element of Di by ;
then f . (X . i) in { z where z is Element of Di : X . i c= z } by A7;
then Intersect Q c= f . (X . i) by ;
then Intersect Q = f . (X . i) by A13;
hence (() .. X) . i = f . (X . i) by A1, A2, A3, A9, Def14
.= (J .. X) . i by ;
:: thesis: verum
end;
hence (ClSys->ClOp ()) .. X = J .. X ; :: thesis: verum
end;
hence ClSys->ClOp () = J by ; :: thesis: verum