let S be 1-sorted ; :: thesis: for D being ClosureSystem of S holds ClOp->ClSys (ClSys->ClOp D) = ClosureStr(# the Sorts of D,the Family of D #)
let D be ClosureSystem of S; :: thesis: ClOp->ClSys (ClSys->ClOp D) = ClosureStr(# the Sorts of D,the Family of D #)
set M = the Sorts of D;
set F = the Family of D;
set d = the Family of (ClOp->ClSys (ClSys->ClOp D));
set f = ClSys->ClOp D;
A1: the Family of (ClOp->ClSys (ClSys->ClOp D)) = { x where x is Element of Bool the Sorts of D : (ClSys->ClOp D) . x = x } by Def23;
the Family of D = the Family of (ClOp->ClSys (ClSys->ClOp D))

proof

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

proof

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in the Family of D or q in the Family of (ClOp->ClSys (ClSys->ClOp D)) )
assume A2: q in the Family of D ; :: thesis: q in the Family of (ClOp->ClSys (ClSys->ClOp D))
then reconsider q1 = q as Element of Bool the Sorts of D ;
consider SF being SubsetFamily of the Sorts of D such that
A3: Cl q1 = meet |:SF:| and
A4: SF = { X where X is Element of Bool the Sorts of D : ( q1 c= X & X in the Family of D ) } by Def24;
A5: q1 c=' the Sorts of D by PBOOLE:def 23;
the Sorts of D in the Family of D by Def9;
then the Sorts of D in SF by A4, A5;
then reconsider SF' = SF as non empty SubsetFamily of the Sorts of D ;

now

let i be set ; :: thesis: ( i in the carrier of S implies ((ClSys->ClOp D) . q1) . i = q1 . i )
assume A6: i in the carrier of S ; :: thesis: ((ClSys->ClOp D) . q1) . i = q1 . i
then consider Q being Subset-Family of (the Sorts of D . i) such that
A7: Q = |:SF':| . i and
A8: (meet |:SF':|) . i = Intersect Q by MSSUBFAM:def 2;
Intersect Q = q1 . i

proof

A9: q1 in SF' by A2, A4;
A10: Q = { (x . i) where x is Element of Bool the Sorts of D : x in SF' } by A6, A7, Th15;
then A11: q1 . i in Q by A9;
hence Intersect Q c= q1 . i by MSSUBFAM:2; :: according to XBOOLE_0:def 10 :: thesis: q1 . i c= Intersect Q

now

let z be set ; :: thesis: ( z in Q implies q1 . i c= z )
assume z in Q ; :: thesis: q1 . i c= z
then consider x being Element of Bool the Sorts of D such that
A12: z = x . i and
A13: x in SF' by A10;
consider xx being Element of Bool the Sorts of D such that
A14: ( xx = x & q1 c=' xx ) and
xx in the Family of D by A4, A13;
thus q1 . i c= z by A6, A12, A14, PBOOLE:def 5; :: thesis: verum

end;

hence q1 . i c= Intersect Q by A11, MSSUBFAM:5; :: thesis: verum

end;

hence ((ClSys->ClOp D) . q1) . i = q1 . i by A3, A8, Def25; :: thesis: verum

end;

then (ClSys->ClOp D) . q1 = q1 by PBOOLE:3;
hence q in the Family of (ClOp->ClSys (ClSys->ClOp D)) by A1; :: thesis: verum

end;

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in the Family of (ClOp->ClSys (ClSys->ClOp D)) or q in the Family of D )
assume q in the Family of (ClOp->ClSys (ClSys->ClOp D)) ; :: thesis: q in the Family of D
then consider x being Element of Bool the Sorts of D such that
A15: q = x and
A16: (ClSys->ClOp D) . x = x by A1;
consider SF being SubsetFamily of the Sorts of D such that
A17: Cl x = meet |:SF:| and
A18: SF = { X where X is Element of Bool the Sorts of D : ( x c=' X & X in the Family of D ) } by Def24;
A19: meet |:SF:| = q by A15, A16, A17, Def25;
defpred S₁[ Element of Bool the Sorts of D] means x c=' $1;
defpred S₂[ Element of Bool the Sorts of D] means ( x c=' $1 & $1 in the Family of D );
defpred S₃[ Element of Bool the Sorts of D] means ( $1 in the Family of D & x c=' $1 );
A20: { H₁(w) where w is Element of Bool the Sorts of D : ( H₁(w) in the Family of D & S₁[w] ) } c= the Family of D from FRAENKEL:sch 17();
A21: for a being Element of Bool the Sorts of D holds
( S₂[a] iff S₃[a] ) ;
{ H₁(a) where a is Element of Bool the Sorts of D : S₂[a] } = { H₁(b) where b is Element of Bool the Sorts of D : S₃[b] } from FRAENKEL:sch 3(A21);
hence q in the Family of D by A18, A19, A20, Def8; :: thesis: verum

end;

hence ClOp->ClSys (ClSys->ClOp D) = ClosureStr(# the Sorts of D,the Family of D #) by Def23; :: thesis: verum