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 Def21;
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 object ; :: 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 Def22;
( q1 c=' the Sorts of D & the Sorts of D in the Family of D ) by Def8, PBOOLE:def 18;
then the Sorts of D in SF by A4;
then reconsider SF9 = SF as non empty SubsetFamily of the Sorts of D ;
now :: thesis: for i being object st i in the carrier of S holds
((ClSys->ClOp D) . q1) . i = q1 . i
let i be object ; :: thesis: ( i in the carrier of S implies ((ClSys->ClOp D) . q1) . i = q1 . i )
assume A5: 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
A6: Q = |:SF9:| . i and
A7: (meet |:SF9:|) . i = Intersect Q by MSSUBFAM:def 1;
A8: Q = { (x . i) where x is Element of Bool the Sorts of D : x in SF9 } by A5, A6, Th14;
q1 in SF9 by A2, A4;
then A9: q1 . i in Q by A8;
then A10: Intersect Q c= q1 . i by MSSUBFAM:2;
now :: thesis: for z being set st z in Q holds
q1 . i c= z
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
A11: z = x . i and
A12: x in SF9 by A8;
ex xx being Element of Bool the Sorts of D st
( xx = x & q1 c=' xx & xx in the Family of D ) by A4, A12;
hence q1 . i c= z by A5, A11; :: thesis: verum
end;
then q1 . i c= Intersect Q by A9, MSSUBFAM:5;
then Intersect Q = q1 . i by A10;
hence ((ClSys->ClOp D) . q1) . i = q1 . i by A3, A7, Def23; :: thesis: verum
end;
then (ClSys->ClOp D) . q1 = q1 ;
hence q in the Family of (ClOp->ClSys (ClSys->ClOp D)) by A1; :: thesis: verum
end;
let q be object ; :: 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
A13: ( q = x & (ClSys->ClOp D) . x = x ) by A1;
defpred S1[ Element of Bool the Sorts of D] means ( $1 in the Family of D & x c=' $1 );
defpred S2[ Element of Bool the Sorts of D] means ( x c=' $1 & $1 in the Family of D );
defpred S3[ Element of Bool the Sorts of D] means x c=' $1;
A14: { H1(w) where w is Element of Bool the Sorts of D : ( H1(w) in the Family of D & S3[w] ) } c= the Family of D from FRAENKEL:sch 17();
 A15: for a being Element of Bool the Sorts of D holds
( S2[a] iff S1[a] ) ;
A16: { H1(a) where a is Element of Bool the Sorts of D : S2[a] } = { H1(b) where b is Element of Bool the Sorts of D : S1[b] } from FRAENKEL:sch 3(A15);
 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 Def22;
meet |:SF:| = q by A13, A17, Def23;
hence q in the Family of D by A18, A14, A16, Def7; :: thesis: verum
end;
hence ClOp->ClSys (ClSys->ClOp D) = ClosureStr(# the Sorts of D, the Family of D #) by Def21; :: thesis: verum