let S be 1-sorted ; :: thesis: for A being ManySortedSet of
for J being reflexive monotonic MSSetOp of A
for D being MSSubsetFamily of A st D = MSFixPoints J holds
MSClosureStr(# A,D #) is MSClosureSystem of S
let A be ManySortedSet of ; :: thesis: for J being reflexive monotonic MSSetOp of A
for D being MSSubsetFamily of A st D = MSFixPoints J holds
MSClosureStr(# A,D #) is MSClosureSystem of S
let J be reflexive monotonic MSSetOp of A; :: thesis: for D being MSSubsetFamily of A st D = MSFixPoints J holds
MSClosureStr(# A,D #) is MSClosureSystem of S
let D be MSSubsetFamily of A; :: thesis: ( D = MSFixPoints J implies MSClosureStr(# A,D #) is MSClosureSystem of S )
assume A1:
D = MSFixPoints J
; :: thesis: MSClosureStr(# A,D #) is MSClosureSystem of S
reconsider CS = MSClosureStr(# A,D #) as MSClosureStr of S ;
CS is absolutely-multiplicative
proof
D is
absolutely-multiplicative
proof
let F be
MSSubsetFamily of
A;
:: according to MSSUBFAM:def 6 :: thesis: ( not F c= D or meet F in D )
assume A2:
F c= D
;
:: thesis: meet F in D
meet F c= A
by PBOOLE:def 23;
then A3:
meet F in bool A
by MBOOLEAN:19;
J .. (meet F) = meet F
proof
thus
J .. (meet F) c= meet F
:: according to PBOOLE:def 13 :: thesis: meet F c= J .. (meet F)proof
let i be
set ;
:: according to PBOOLE:def 5 :: thesis: ( not i in the carrier of S or (J .. (meet F)) . i c= (meet F) . i )
assume A4:
i in the
carrier of
S
;
:: thesis: (J .. (meet F)) . i c= (meet F) . i
then reconsider j =
J . i as
Function of
((bool A) . i),
((bool A) . i) by PBOOLE:def 18;
consider Q being
Subset-Family of
(A . i) such that A5:
(
Q = F . i &
(meet F) . i = Intersect Q )
by A4, MSSUBFAM:def 2;
A6:
i in dom J
by A4, PARTFUN1:def 4;
(bool A) . i = bool (A . i)
by A4, MBOOLEAN:def 1;
then A7:
j . (Intersect Q) in bool (A . i)
by FUNCT_2:7;
now let x be
set ;
:: thesis: ( x in Q implies j . (Intersect Q) c= x )assume A8:
x in Q
;
:: thesis: j . (Intersect Q) c= x
Q c= D . i
by A2, A4, A5, PBOOLE:def 5;
then consider jj being
Function such that A9:
(
jj = J . i &
x in dom jj &
jj . x = x )
by A1, A4, A8, Def13;
thus
j . (Intersect Q) c= x
by A4, A8, A9, Th25, MSSUBFAM:2;
:: thesis: verum end;
then
j . (Intersect Q) c= Intersect Q
by A7, MSSUBFAM:4;
hence
(J .. (meet F)) . i c= (meet F) . i
by A5, A6, PRALG_1:def 17;
:: thesis: verum
end;
meet F is
Element of
bool A
by A3, MSSUBFAM:11;
hence
meet F c= J .. (meet F)
by Def2;
:: thesis: verum
end;
hence
meet F in D
by A1, A3, Th28;
:: thesis: verum
end;
hence
the
Family of
CS is
absolutely-multiplicative
;
:: according to CLOSURE1:def 9 :: thesis: verum
end;
hence
MSClosureStr(# A,D #) is MSClosureSystem of S
; :: thesis: verum