let S be 1-sorted ; :: thesis: for D being ClosureSystem of S
for f being SetOp of the Sorts of D st ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) holds
( f is reflexive & f is monotonic & f is idempotent )
let D be ClosureSystem of S; :: thesis: for f being SetOp of the Sorts of D st ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) holds
( f is reflexive & f is monotonic & f is idempotent )
let f be SetOp of the Sorts of D; :: thesis: ( ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) implies ( f is reflexive & f is monotonic & f is idempotent ) )
assume A1: for x being Element of Bool the Sorts of D holds f . x = Cl x ; :: thesis: ( f is reflexive & f is monotonic & f is idempotent )
set M = the Sorts of D;
A2: f is reflexive

proof

let x be Element of Bool the Sorts of D; :: according to CLOSURE2:def 12 :: thesis: x c=' f . x
consider F being SubsetFamily of the Sorts of D such that
A3: Cl x = meet |:F:| and
A4: F = { X where X is Element of Bool the Sorts of D : ( x c=' X & X in the Family of D ) } by Def24;
A5: for Z1 being ManySortedSet of the carrier of S st Z1 in F holds
x c=' Z1

proof

let Z1 be ManySortedSet of the carrier of S; :: thesis: ( Z1 in F implies x c=' Z1 )
assume Z1 in F ; :: thesis: x c=' Z1
then consider a being Element of Bool the Sorts of D such that
A6: ( Z1 = a & x c=' a ) and
a in the Family of D by A4;
thus x c=' Z1 by A6; :: thesis: verum

end;

f . x = meet |:F:| by A1, A3;
hence x c=' f . x by A5, Th25; :: thesis: verum

end;

A7: f is monotonic

proof

let x, y be Element of Bool the Sorts of D; :: according to CLOSURE2:def 13 :: thesis: ( x c=' y implies f . x c=' f . y )
assume A8: x c=' y ; :: thesis: f . x c=' f . y
consider Fx being SubsetFamily of the Sorts of D such that
A9: Cl x = meet |:Fx:| and
A10: Fx = { X where X is Element of Bool the Sorts of D : ( x c=' X & X in the Family of D ) } by Def24;
consider Fy being SubsetFamily of the Sorts of D such that
A11: Cl y = meet |:Fy:| and
A12: Fy = { X where X is Element of Bool the Sorts of D : ( y c=' X & X in the Family of D ) } by Def24;
|:Fy:| c=' |:Fx:|

proof

let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in the carrier of S or |:Fy:| . i c= |:Fx:| . i )
assume A13: i in the carrier of S ; :: thesis: |:Fy:| . i c= |:Fx:| . i
thus |:Fy:| . i c= |:Fx:| . i :: thesis: verum

proof

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in |:Fy:| . i or q in |:Fx:| . i )
assume A14: q in |:Fy:| . i ; :: thesis: q in |:Fx:| . i

per cases ( Fy is empty or not Fy is empty ) ;

suppose Fy is empty ; :: thesis: q in |:Fx:| . i

then reconsider Fy' = Fy as empty SubsetFamily of the Sorts of D ;
|:Fy':| . i is empty by A13, PBOOLE:def 15;
hence q in |:Fx:| . i by A14; :: thesis: verum

end;

suppose not Fy is empty ; :: thesis: q in |:Fx:| . i

then |:Fy:| . i = { (e . i) where e is Element of Bool the Sorts of D : e in Fy } by A13, Th15;
then consider w being Element of Bool the Sorts of D such that
A15: q = w . i and
A16: w in Fy by A14;
consider r being Element of Bool the Sorts of D such that
A17: r = w and
A18: y c=' r and
A19: r in the Family of D by A12, A16;
x c=' w by A8, A17, A18, PBOOLE:15;
then A20: w in Fx by A10, A17, A19;
then |:Fx:| . i = { (e . i) where e is Element of Bool the Sorts of D : e in Fx } by A13, Th15;
hence q in |:Fx:| . i by A15, A20; :: thesis: verum

end;

end;

end;

end;

then meet |:Fx:| c=' meet |:Fy:| by MSSUBFAM:46;
then meet |:Fx:| c=' f . y by A1, A11;
hence f . x c=' f . y by A1, A9; :: thesis: verum

end;

f is idempotent

proof

let x be Element of Bool the Sorts of D; :: according to CLOSURE2:def 14 :: thesis: f . x = f . (f . x)
consider F being SubsetFamily of the Sorts of D such that
A21: Cl x = meet |:F:| and
A22: F = { X where X is Element of Bool the Sorts of D : ( x c=' X & X in the Family of D ) } by Def24;
F c= the Family of D

proof

let k be set ; :: according to TARSKI:def 3 :: thesis: ( not k in F or k in the Family of D )
assume k in F ; :: thesis: k in the Family of D
then consider q being Element of Bool the Sorts of D such that
A23: ( k = q & x c=' q & q in the Family of D ) by A22;
thus k in the Family of D by A23; :: thesis: verum

end;

then A24: meet |:F:| in the Family of D by Def8;
thus f . x = meet |:F:| by A1, A21
.= f . (meet |:F:|) by A1, A24, Th40
.= f . (f . x) by A1, A21 ; :: thesis: verum

end;

hence ( f is reflexive & f is monotonic & f is idempotent ) by A2, A7; :: thesis: verum