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 () = the carrier of S by PARTFUN1:def 2;
rng () c= bool (Union the Sorts of MA)
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in rng () or u in bool (Union the Sorts of MA) )
reconsider uu = u as set by TARSKI:1;
assume u in rng () ; :: thesis: u in bool (Union the Sorts of MA)
then consider i being object such that
A3: i in dom () and
A4: u = () . 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 ;
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 ;
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 ;
reconsider x = meet |:F:| as MSSubset of MA ;
for B being MSSubset of MA st B = x holds
B is opers_closed by ;
hence meet |:F:| in SUBMA by ; :: thesis: verum
end;
hence SubSort MA is absolutely-multiplicative SubsetFamily of the Sorts of MA by CLOSURE2:def 7; :: thesis: verum