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 a in the Family of D & ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) holds
f . a = a
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 a in the Family of D & ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) holds
f . a = a
let a be Element of Bool the Sorts of D; :: thesis: for f being SetOp of the Sorts of D st a in the Family of D & ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) holds
f . a = a
let f be SetOp of the Sorts of D; :: thesis: ( a in the Family of D & ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) implies f . a = a )
assume that
A1: a in the Family of D and
A2: for x being Element of Bool the Sorts of D holds f . x = Cl x ; :: thesis: f . a = a
consider F being SubsetFamily of the Sorts of D such that
A3: Cl a = meet |:F:| and
A4: F = { X where X is Element of Bool the Sorts of D : ( a c=' X & X in the Family of D ) } by Def22;
A5: f . a = meet |:F:| by A2, A3;
a in F by A1, A4;
then A6: f . a c= a by A5, Th21, MSSUBFAM:43;
for Z1 being ManySortedSet of the carrier of S st Z1 in F holds
a c=' Z1
proof
let Z1 be ManySortedSet of the carrier of S; :: thesis: ( Z1 in F implies a c=' Z1 )
assume Z1 in F ; :: thesis: a c=' Z1
then ex b being Element of Bool the Sorts of D st
( Z1 = b & a c=' b & b in the Family of D ) by A4;
hence a c=' Z1 ; :: thesis: verum
end;
then a c= f . a by A5, Th24;
hence f . a = a by A6, PBOOLE:146; :: thesis: verum