let S be 1-sorted ; :: thesis: for A being ManySortedSet of
for f being ClosureOperator of A holds ClSys->ClOp (ClOp->ClSys f) = f
let A be ManySortedSet of ; :: thesis: for f being ClosureOperator of A holds ClSys->ClOp (ClOp->ClSys f) = f
let f be ClosureOperator of A; :: thesis: ClSys->ClOp (ClOp->ClSys f) = f
set D = ClOp->ClSys f;
set M = the Sorts of (ClOp->ClSys f);
set f1 = ClSys->ClOp (ClOp->ClSys f);
A1: A = the Sorts of (ClOp->ClSys f) by Def23;
then reconsider ff = f as reflexive monotonic idempotent SetOp of the Sorts of (ClOp->ClSys f) ;
for x being set st x in Bool A holds
(ClSys->ClOp (ClOp->ClSys f)) . x = ff . x

proof

let x be set ; :: thesis: ( x in Bool A implies (ClSys->ClOp (ClOp->ClSys f)) . x = ff . x )
assume x in Bool A ; :: thesis: (ClSys->ClOp (ClOp->ClSys f)) . x = ff . x
then reconsider x1 = x as Element of Bool the Sorts of (ClOp->ClSys f) by Def23;
consider F being SubsetFamily of the Sorts of (ClOp->ClSys f) such that
A2: Cl x1 = meet |:F:| and
A3: F = { X where X is Element of Bool the Sorts of (ClOp->ClSys f) : ( x1 c=' X & X in the Family of (ClOp->ClSys f) ) } by Def24;

A4: now

let i be set ; :: thesis: ( i in the carrier of S implies (meet |:F:|) . i = (ff . x1) . i )
assume A5: i in the carrier of S ; :: thesis: (meet |:F:|) . i = (ff . x1) . i
then consider Q being Subset-Family of (the Sorts of (ClOp->ClSys f) . i) such that
A6: Q = |:F:| . i and
A7: (meet |:F:|) . i = Intersect Q by MSSUBFAM:def 2;
A8: x1 c=' the Sorts of (ClOp->ClSys f) by PBOOLE:def 23;
the Sorts of (ClOp->ClSys f) in the Family of (ClOp->ClSys f) by Def9;
then the Sorts of (ClOp->ClSys f) in F by A3, A8;
then reconsider F' = F as non empty SubsetFamily of the Sorts of (ClOp->ClSys f) ;
thus (meet |:F:|) . i = (ff . x1) . i :: thesis: verum

proof

A9: Q = { (q . i) where q is Element of Bool the Sorts of (ClOp->ClSys f) : q in F' } by A5, A6, Th15;
A10: the Family of (ClOp->ClSys f) = { q where q is Element of Bool the Sorts of (ClOp->ClSys f) : ff . q = q } by A1, Def23;
ff . (ff . x1) = ff . x1 by Def14;
then A11: ff . x1 in the Family of (ClOp->ClSys f) by A10;
x1 c=' ff . x1 by Def12;
then ff . x1 in F' by A3, A11;
then (ff . x1) . i in Q by A9;
hence (meet |:F:|) . i c= (ff . x1) . i by A7, MSSUBFAM:2; :: according to XBOOLE_0:def 10 :: thesis: (ff . x1) . i c= (meet |:F:|) . i
Q = |:F':| . i by A6;
then A12: not Q is empty by A5;

now

let z be set ; :: thesis: ( z in Q implies (ff . x1) . i c= z )
assume z in Q ; :: thesis: (ff . x1) . i c= z
then consider q being Element of Bool the Sorts of (ClOp->ClSys f) such that
A13: z = q . i and
A14: q in F' by A9;
consider X being Element of Bool the Sorts of (ClOp->ClSys f) such that
A15: q = X and
A16: x1 c=' X and
A17: X in the Family of (ClOp->ClSys f) by A3, A14;
consider t being Element of Bool the Sorts of (ClOp->ClSys f) such that
A18: X = t and
A19: ff . t = t by A10, A17;
ff . x1 c=' ff . X by A16, Def13;
hence (ff . x1) . i c= z by A5, A13, A15, A18, A19, PBOOLE:def 5; :: thesis: verum

end;

hence (ff . x1) . i c= (meet |:F:|) . i by A7, A12, MSSUBFAM:5; :: thesis: verum

end;

end;

thus (ClSys->ClOp (ClOp->ClSys f)) . x = Cl x1 by Def25
.= ff . x by A2, A4, PBOOLE:3 ; :: thesis: verum

end;

hence ClSys->ClOp (ClOp->ClSys f) = f by A1, FUNCT_2:18; :: thesis: verum