let S be 1-sorted ; :: thesis: for D being ClosureSystem of S
for a being Element of Bool the Sorts of D
for f being SetOp of the Sorts of D st f . a = a & ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) holds
a in the Family of D
deffunc H₁( set ) -> set = $1;
let D be ClosureSystem of S; :: thesis: for a being Element of Bool the Sorts of D
for f being SetOp of the Sorts of D st f . a = a & ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) holds
a in the Family of D
let a be Element of Bool the Sorts of D; :: thesis: for f being SetOp of the Sorts of D st f . a = a & ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) holds
a in the Family of D
let f be SetOp of the Sorts of D; :: thesis: ( f . a = a & ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) implies a in the Family of D )
assume A1: ( f . a = a & ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) ) ; :: thesis: a in the Family of D
set F = the Family of D;
set M = the Sorts of D;
defpred S₁[ Element of Bool the Sorts of D] means a c=' $1;
defpred S₂[ Element of Bool the Sorts of D] means ( a c=' $1 & $1 in the Family of D );
defpred S₃[ Element of Bool the Sorts of D] means ( $1 in the Family of D & a c=' $1 );
A2: { 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();
A3: for q being Element of Bool the Sorts of D holds
( S₂[q] iff S₃[q] ) ;
A4: { H₁(s) where s is Element of Bool the Sorts of D : S₂[s] } = { H₁(b) where b is Element of Bool the Sorts of D : S₃[b] } from FRAENKEL:sch 3(A3);
consider SF being SubsetFamily of the Sorts of D such that
A5: Cl a = meet |:SF:| and
A6: SF = { X where X is Element of Bool the Sorts of D : ( a c= X & X in the Family of D ) } by Def22;
a = meet |:SF:| by A1, A5;
hence a in the Family of D by A6, A2, A4, Def7; :: thesis: verum