let S be non empty non void ManySortedSign ; :: thesis: for MA being strict non-empty MSAlgebra over S holds SubSort MA is absolutely-multiplicative SubsetFamily of the Sorts of MA

let MA be strict non-empty MSAlgebra over S; :: thesis: SubSort MA is absolutely-multiplicative SubsetFamily of the Sorts of MA

SubSort MA c= Bool the Sorts of MA

for F being SubsetFamily of the Sorts of MA st F c= SUBMA holds

meet |:F:| in SUBMA

let MA be strict non-empty MSAlgebra over S; :: thesis: SubSort MA is absolutely-multiplicative SubsetFamily of the Sorts of MA

SubSort MA c= Bool the Sorts of MA

proof

then reconsider SUBMA = SubSort MA as SubsetFamily of the Sorts of MA ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in SubSort MA or x in Bool the Sorts of MA )

assume x in SubSort MA ; :: thesis: x in Bool the Sorts of MA

then x is ManySortedSubset of the Sorts of MA by MSUALG_2:def 11;

hence x in Bool the Sorts of MA by CLOSURE2:def 1; :: thesis: verum

end;assume x in SubSort MA ; :: thesis: x in Bool the Sorts of MA

then x is ManySortedSubset of the Sorts of MA by MSUALG_2:def 11;

hence x in Bool the Sorts of MA by CLOSURE2:def 1; :: thesis: verum

for F being SubsetFamily of the Sorts of MA st F c= SUBMA holds

meet |:F:| in SUBMA

proof

hence
SubSort MA is absolutely-multiplicative SubsetFamily of the Sorts of MA
by CLOSURE2:def 7; :: thesis: verum
set M = bool (Union the Sorts of MA);

set I = the carrier of S;

let F be SubsetFamily of the Sorts of MA; :: thesis: ( F c= SUBMA implies meet |:F:| in SUBMA )

assume A1: F c= SUBMA ; :: thesis: meet |:F:| in SUBMA

set x = meet |:F:|;

A2: dom (meet |:F:|) = the carrier of S by PARTFUN1:def 2;

rng (meet |:F:|) c= bool (Union the Sorts of MA)

reconsider x = meet |:F:| as MSSubset of MA ;

for B being MSSubset of MA st B = x holds

B is opers_closed by A1, Th3;

hence meet |:F:| in SUBMA by A6, MSUALG_2:def 11; :: thesis: verum

end;set I = the carrier of S;

let F be SubsetFamily of the Sorts of MA; :: thesis: ( F c= SUBMA implies meet |:F:| in SUBMA )

assume A1: F c= SUBMA ; :: thesis: meet |:F:| in SUBMA

set x = meet |:F:|;

A2: dom (meet |:F:|) = the carrier of S by PARTFUN1:def 2;

rng (meet |:F:|) c= bool (Union the Sorts of MA)

proof

then A6:
meet |:F:| in Funcs ( the carrier of S,(bool (Union the Sorts of MA)))
by A2, FUNCT_2:def 2;
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in rng (meet |:F:|) or u in bool (Union the Sorts of MA) )

reconsider uu = u as set by TARSKI:1;

assume u in rng (meet |:F:|) ; :: thesis: u in bool (Union the Sorts of MA)

then consider i being object such that

A3: i in dom (meet |:F:|) and

A4: u = (meet |:F:|) . i by FUNCT_1:def 3;

dom the Sorts of MA = the carrier of S by PARTFUN1:def 2;

then the Sorts of MA . i in rng the Sorts of MA by A2, A3, FUNCT_1:def 3;

then A5: the Sorts of MA . i c= union (rng the Sorts of MA) by ZFMISC_1:74;

ex Q being Subset-Family of ( the Sorts of MA . i) st

( Q = |:F:| . i & u = Intersect Q ) by A2, A3, A4, MSSUBFAM:def 1;

then uu c= union (rng the Sorts of MA) by A5;

then u in bool (union (rng the Sorts of MA)) ;

hence u in bool (Union the Sorts of MA) by CARD_3:def 4; :: thesis: verum

end;reconsider uu = u as set by TARSKI:1;

assume u in rng (meet |:F:|) ; :: thesis: u in bool (Union the Sorts of MA)

then consider i being object such that

A3: i in dom (meet |:F:|) and

A4: u = (meet |:F:|) . i by FUNCT_1:def 3;

dom the Sorts of MA = the carrier of S by PARTFUN1:def 2;

then the Sorts of MA . i in rng the Sorts of MA by A2, A3, FUNCT_1:def 3;

then A5: the Sorts of MA . i c= union (rng the Sorts of MA) by ZFMISC_1:74;

ex Q being Subset-Family of ( the Sorts of MA . i) st

( Q = |:F:| . i & u = Intersect Q ) by A2, A3, A4, MSSUBFAM:def 1;

then uu c= union (rng the Sorts of MA) by A5;

then u in bool (union (rng the Sorts of MA)) ;

hence u in bool (Union the Sorts of MA) by CARD_3:def 4; :: thesis: verum

reconsider x = meet |:F:| as MSSubset of MA ;

for B being MSSubset of MA st B = x holds

B is opers_closed by A1, Th3;

hence meet |:F:| in SUBMA by A6, MSUALG_2:def 11; :: thesis: verum