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
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 that
A1:
f . a = a
and
A2:
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;
consider SF being SubsetFamily of the Sorts of D such that
A3:
Cl a = meet |:SF:|
and
A4:
SF = { X where X is Element of Bool the Sorts of D : ( a c= X & X in the Family of D ) }
by Def24;
A5:
a = meet |:SF:|
by A1, A2, A3;
deffunc H1( set ) -> set = $1;
defpred S1[ Element of Bool the Sorts of D] means a c=' $1;
defpred S2[ Element of Bool the Sorts of D] means ( a c=' $1 & $1 in the Family of D );
defpred S3[ Element of Bool the Sorts of D] means ( $1 in the Family of D & a c=' $1 );
A6:
{ H1(w) where w is Element of Bool the Sorts of D : ( H1(w) in the Family of D & S1[w] ) } c= the Family of D
from FRAENKEL:sch 17();
A7:
for q being Element of Bool the Sorts of D holds
( S2[q] iff S3[q] )
;
{ H1(s) where s is Element of Bool the Sorts of D : S2[s] } = { H1(b) where b is Element of Bool the Sorts of D : S3[b] }
from FRAENKEL:sch 3(A7);
hence
a in the Family of D
by A4, A5, A6, Def8; :: thesis: verum