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

proof

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;

then reconsider SUBMA = SubSort MA as SubsetFamily of the Sorts of MA ;
for F being SubsetFamily of the Sorts of MA st F c= SUBMA holds
meet |:F:| in SUBMA

proof

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)

proof

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;

then A6: meet |:F:| in Funcs ( the carrier of S,(bool (Union the Sorts of MA))) by A2, FUNCT_2:def 2;
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;

hence SubSort MA is absolutely-multiplicative SubsetFamily of the Sorts of MA by CLOSURE2:def 7; :: thesis: verum