let S be 1-sorted ; :: thesis: for A being ManySortedSet of the carrier of S
for f being ClosureOperator of A holds ClSys->ClOp (ClOp->ClSys f) = f
let A be ManySortedSet of the carrier of S; :: 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 Def21;
then reconsider ff = f as reflexive monotonic idempotent SetOp of the Sorts of (ClOp->ClSys f) ;
for x being object st x in Bool A holds
(ClSys->ClOp (ClOp->ClSys f)) . x = ff . x
proof
let x be object ; :: 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 Def21;
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 Def22;
A4: now :: thesis: for i being object st i in the carrier of S holds
(meet |:F:|) . i = (ff . x1) . i
A5: x1 c=' ff . x1 by Def10;
( x1 c=' the Sorts of (ClOp->ClSys f) & the Sorts of (ClOp->ClSys f) in the Family of (ClOp->ClSys f) ) by Def8, PBOOLE:def 18;
then the Sorts of (ClOp->ClSys f) in F by A3;
then reconsider F9 = F as non empty SubsetFamily of the Sorts of (ClOp->ClSys f) ;
let i be object ; :: thesis: ( i in the carrier of S implies (meet |:F:|) . i = (ff . x1) . i )
assume A6: 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
A7: Q = |:F:| . i and
A8: (meet |:F:|) . i = Intersect Q by MSSUBFAM:def 1;
A9: Q = { (q . i) where q is Element of Bool the Sorts of (ClOp->ClSys f) : q in F9 } by A6, A7, Th14;
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, Def21;
A11: now :: thesis: for z being set st z in Q holds
(ff . x1) . i c= z
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
A12: z = q . i and
A13: q in F9 by A9;
consider X being Element of Bool the Sorts of (ClOp->ClSys f) such that
A14: q = X and
A15: ( x1 c=' X & X in the Family of (ClOp->ClSys f) ) by A3, A13;
( ex t being Element of Bool the Sorts of (ClOp->ClSys f) st
( X = t & ff . t = t ) & ff . x1 c=' ff . X ) by A10, A15, Def11;
hence (ff . x1) . i c= z by A6, A12, A14; :: thesis: verum
end;
ff . (ff . x1) = ff . x1 by Def12;
then ff . x1 in the Family of (ClOp->ClSys f) by A10;
then ff . x1 in F9 by A3, A5;
then (ff . x1) . i in Q by A9;
then A16: (meet |:F:|) . i c= (ff . x1) . i by A8, MSSUBFAM:2;
Q = |:F9:| . i by A7;
then (ff . x1) . i c= (meet |:F:|) . i by A6, A8, A11, MSSUBFAM:5;
hence (meet |:F:|) . i = (ff . x1) . i by A16; :: thesis: verum
end;
thus (ClSys->ClOp (ClOp->ClSys f)) . x = Cl x1 by Def23
.= ff . x by A2, A4, PBOOLE:3 ; :: thesis: verum
end;
hence ClSys->ClOp (ClOp->ClSys f) = f by A1, FUNCT_2:12; :: thesis: verum