:: MSSUBFAM semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let I be set ;
let F be ManySortedFunction of I;
:: original: doms
redefine func doms F -> ManySortedSet of I;
coherence
doms F is ManySortedSet of I
proof end;
:: original: rngs
redefine func rngs F -> ManySortedSet of I;
coherence
rngs F is ManySortedSet of I
proof end;
end;

scheme :: MSSUBFAM:sch 1
MSFExFunc{ F1() -> set , F2() -> ManySortedSet of F1(), F3() -> ManySortedSet of F1(), P1[ set , set , set ] } :
ex F being ManySortedFunction of F2(),F3() st
for i being set st i in F1() holds
ex f being Function of F2() . i,F3() . i st
( f = F . i & ( for x being set st x in F2() . i holds
P1[f . x,x,i] ) )
provided
A1: for i being set st i in F1() holds
for x being set st x in F2() . i holds
ex y being set st
( y in F3() . i & P1[y,x,i] )
proof end;

theorem :: MSSUBFAM:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for sf being Subset-Family of I st sf <> {} holds
Intersect sf c= union sf
proof end;

theorem :: MSSUBFAM:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I, G being set
for sf being Subset-Family of I st G in sf holds
Intersect sf c= G
proof end;

theorem :: MSSUBFAM:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for sf being Subset-Family of I st {} in sf holds
Intersect sf = {}
proof end;

theorem :: MSSUBFAM:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for sf being Subset-Family of I
for Z being Subset of I st ( for Z1 being set st Z1 in sf holds
Z c= Z1 ) holds
Z c= Intersect sf
proof end;

theorem :: MSSUBFAM:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I, G being set
for sf being Subset-Family of I st sf <> {} & ( for Z1 being set st Z1 in sf holds
G c= Z1 ) holds
G c= Intersect sf
proof end;

theorem :: MSSUBFAM:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I, G, H being set
for sf being Subset-Family of I st G in sf & G c= H holds
Intersect sf c= H
proof end;

theorem :: MSSUBFAM:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I, G, H being set
for sf being Subset-Family of I st G in sf & G misses H holds
Intersect sf misses H
proof end;

theorem :: MSSUBFAM:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for sh, sf, sg being Subset-Family of I st sh = sf \/ sg holds
Intersect sh = (Intersect sf) /\ (Intersect sg)
proof end;

theorem :: MSSUBFAM:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for sf being Subset-Family of I
for v being Subset of I st sf = {v} holds
Intersect sf = v
proof end;

theorem :: MSSUBFAM:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for sf being Subset-Family of I
for v, w being Subset of I st sf = {v,w} holds
Intersect sf = v /\ w
proof end;

theorem :: MSSUBFAM:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A, B being ManySortedSet of I st A in B holds
A is Element of B
proof end;

theorem :: MSSUBFAM:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A being ManySortedSet of I
for B being V3 ManySortedSet of I st A is Element of B holds
A in B
proof end;

theorem Th13: :: MSSUBFAM:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, I being set
for F being ManySortedFunction of I
for f being Function st i in I & f = F . i holds
(rngs F) . i = rng f
proof end;

theorem Th14: :: MSSUBFAM:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, I being set
for F being ManySortedFunction of I
for f being Function st i in I & f = F . i holds
(doms F) . i = dom f
proof end;

theorem :: MSSUBFAM:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for F, G being ManySortedFunction of I holds G ** F is ManySortedFunction of I
proof end;

theorem :: MSSUBFAM:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A being V3 ManySortedSet of I
for F being ManySortedFunction of A, [0] I holds F = [0] I
proof end;

theorem :: MSSUBFAM:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A, B being ManySortedSet of I
for F being ManySortedFunction of I st A is_transformable_to B & F is ManySortedFunction of A,B holds
( doms F = A & rngs F c= B )
proof end;

registration
let I be set ;
cluster V4 -> locally-finite ManySortedSet of I;
coherence
for b1 being ManySortedSet of I st b1 is empty-yielding holds
b1 is locally-finite
proof end;
end;

registration
let I be set ;
cluster [0] I -> V4 locally-finite ;
coherence
( [0] I is empty-yielding & [0] I is locally-finite )
;
end;

registration
let I be set ;
let A be ManySortedSet of I;
cluster V4 locally-finite ManySortedSubset of A;
existence
ex b1 being ManySortedSubset of A st
( b1 is empty-yielding & b1 is locally-finite )
proof end;
end;

theorem Th18: :: MSSUBFAM:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A, B being ManySortedSet of I st A c= B & B is locally-finite holds
A is locally-finite
proof end;

registration
let I be set ;
let A be locally-finite ManySortedSet of I;
cluster -> locally-finite ManySortedSubset of A;
coherence
for b1 being ManySortedSubset of A holds b1 is locally-finite
proof end;
end;

registration
let I be set ;
let A, B be locally-finite ManySortedSet of I;
cluster A \/ B -> locally-finite ;
coherence
A \/ B is locally-finite
proof end;
end;

registration
let I be set ;
let A be ManySortedSet of I;
let B be locally-finite ManySortedSet of I;
cluster A /\ B -> locally-finite ;
coherence
A /\ B is locally-finite
proof end;
end;

registration
let I be set ;
let B be ManySortedSet of I;
let A be locally-finite ManySortedSet of I;
cluster A /\ B -> locally-finite ;
coherence
A /\ B is locally-finite
;
end;

registration
let I be set ;
let B be ManySortedSet of I;
let A be locally-finite ManySortedSet of I;
cluster A \ B -> locally-finite ;
coherence
A \ B is locally-finite
proof end;
end;

registration
let I be set ;
let F be ManySortedFunction of I;
let A be locally-finite ManySortedSet of I;
cluster F .:.: A -> locally-finite ;
coherence
F .:.: A is locally-finite
proof end;
end;

registration
let I be set ;
let A, B be locally-finite ManySortedSet of I;
cluster [|A,B|] -> locally-finite ;
coherence
[|A,B|] is locally-finite
proof end;
end;

theorem :: MSSUBFAM:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for B, A being ManySortedSet of I st B is non-empty & [|A,B|] is locally-finite holds
A is locally-finite
proof end;

theorem :: MSSUBFAM:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A, B being ManySortedSet of I st A is non-empty & [|A,B|] is locally-finite holds
B is locally-finite
proof end;

theorem Th21: :: MSSUBFAM:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A being ManySortedSet of I holds
( A is locally-finite iff bool A is locally-finite )
proof end;

registration
let I be set ;
let M be locally-finite ManySortedSet of I;
cluster bool M -> locally-finite ;
coherence
bool M is locally-finite
by Th21;
end;

theorem :: MSSUBFAM:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A being V3 ManySortedSet of I st A is locally-finite & ( for M being ManySortedSet of I st M in A holds
M is locally-finite ) holds
union A is locally-finite
proof end;

theorem :: MSSUBFAM:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A being ManySortedSet of I st union A is locally-finite holds
( A is locally-finite & ( for M being ManySortedSet of I st M in A holds
M is locally-finite ) )
proof end;

theorem :: MSSUBFAM:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for F being ManySortedFunction of I st doms F is locally-finite holds
rngs F is locally-finite
proof end;

theorem :: MSSUBFAM:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A being ManySortedSet of I
for F being ManySortedFunction of I st A c= rngs F & ( for i being set
for f being Function st i in I & f = F . i holds
f " (A . i) is finite ) holds
A is locally-finite
proof end;

registration
let I be set ;
let A, B be locally-finite ManySortedSet of I;
cluster MSFuncs A,B -> locally-finite ;
coherence
MSFuncs A,B is locally-finite
proof end;
end;

registration
let I be set ;
let A, B be locally-finite ManySortedSet of I;
cluster A \+\ B -> locally-finite ;
coherence
A \+\ B is locally-finite
;
end;

theorem :: MSSUBFAM:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y, Z being ManySortedSet of I st X is locally-finite & X c= [|Y,Z|] holds
ex A, B being ManySortedSet of I st
( A is locally-finite & A c= Y & B is locally-finite & B c= Z & X c= [|A,B|] )
proof end;

theorem :: MSSUBFAM:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Z, Y being ManySortedSet of I st X is locally-finite & Z is locally-finite & X c= [|Y,Z|] holds
ex A being ManySortedSet of I st
( A is locally-finite & A c= Y & X c= [|A,Z|] )
proof end;

theorem :: MSSUBFAM:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for M being V3 locally-finite ManySortedSet of I st ( for A, B being ManySortedSet of I st A in M & B in M & not A c= B holds
B c= A ) holds
ex m being ManySortedSet of I st
( m in M & ( for K being ManySortedSet of I st K in M holds
m c= K ) )
proof end;

theorem :: MSSUBFAM:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for M being V3 locally-finite ManySortedSet of I st ( for A, B being ManySortedSet of I st A in M & B in M & not A c= B holds
B c= A ) holds
ex m being ManySortedSet of I st
( m in M & ( for K being ManySortedSet of I st K in M holds
K c= m ) )
proof end;

theorem :: MSSUBFAM:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for F being ManySortedFunction of I
for Z being ManySortedSet of I st Z is locally-finite & Z c= rngs F holds
ex Y being ManySortedSet of I st
( Y c= doms F & Y is locally-finite & F .:.: Y = Z )
proof end;

definition
let I be set ;
let M be ManySortedSet of I;
mode MSSubsetFamily of M is ManySortedSubset of bool M;
end;

registration
let I be set ;
let M be ManySortedSet of I;
cluster V3 ManySortedSubset of bool M;
existence
ex b1 being MSSubsetFamily of M st b1 is non-empty
proof end;
end;

definition
let I be set ;
let M be ManySortedSet of I;
:: original: bool
redefine func bool M -> MSSubsetFamily of M;
coherence
bool M is MSSubsetFamily of M
by PBOOLE:def 23;
end;

registration
let I be set ;
let M be ManySortedSet of I;
cluster V4 locally-finite ManySortedSubset of bool M;
existence
ex b1 being MSSubsetFamily of M st
( b1 is empty-yielding & b1 is locally-finite )
proof end;
end;

theorem :: MSSUBFAM:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for M being ManySortedSet of I holds [0] I is V4 locally-finite MSSubsetFamily of M
proof end;

registration
let I be set ;
let M be locally-finite ManySortedSet of I;
cluster V3 locally-finite ManySortedSubset of bool M;
existence
ex b1 being MSSubsetFamily of M st
( b1 is non-empty & b1 is locally-finite )
proof end;
end;

definition
let I be non empty set ;
let M be ManySortedSet of I;
let SF be MSSubsetFamily of M;
let i be Element of I;
:: original: .
redefine func SF . i -> Subset-Family of (M . i);
coherence
SF . i is Subset-Family of (M . i)
proof end;
end;

theorem Th32: :: MSSUBFAM:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, I being set
for M being ManySortedSet of I
for SF being MSSubsetFamily of M st i in I holds
SF . i is Subset-Family of (M . i)
proof end;

theorem Th33: :: MSSUBFAM:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A, M being ManySortedSet of I
for SF being MSSubsetFamily of M st A in SF holds
A is ManySortedSubset of M
proof end;

theorem Th34: :: MSSUBFAM:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for M being ManySortedSet of I
for SF, SG being MSSubsetFamily of M holds SF \/ SG is MSSubsetFamily of M
proof end;

theorem :: MSSUBFAM:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for M being ManySortedSet of I
for SF, SG being MSSubsetFamily of M holds SF /\ SG is MSSubsetFamily of M
proof end;

theorem Th36: :: MSSUBFAM:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A, M being ManySortedSet of I
for SF being MSSubsetFamily of M holds SF \ A is MSSubsetFamily of M
proof end;

theorem :: MSSUBFAM:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for M being ManySortedSet of I
for SF, SG being MSSubsetFamily of M holds SF \+\ SG is MSSubsetFamily of M
proof end;

theorem Th38: :: MSSUBFAM:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A, M being ManySortedSet of I st A c= M holds
{A} is MSSubsetFamily of M
proof end;

theorem Th39: :: MSSUBFAM:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A, M, B being ManySortedSet of I st A c= M & B c= M holds
{A,B} is MSSubsetFamily of M
proof end;

theorem Th40: :: MSSUBFAM:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for M being ManySortedSet of I
for SF being MSSubsetFamily of M holds union SF c= M
proof end;

definition
let I be set ;
let M be ManySortedSet of I;
let SF be MSSubsetFamily of M;
canceled;
func meet SF -> ManySortedSet of I means :Def2: :: MSSUBFAM:def 2
for i being set st i in I holds
ex Q being Subset-Family of (M . i) st
( Q = SF . i & it . i = Intersect Q );
existence
ex b1 being ManySortedSet of I st
for i being set st i in I holds
ex Q being Subset-Family of (M . i) st
( Q = SF . i & b1 . i = Intersect Q )
proof end;
uniqueness
for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds
ex Q being Subset-Family of (M . i) st
( Q = SF . i & b1 . i = Intersect Q ) ) & ( for i being set st i in I holds
ex Q being Subset-Family of (M . i) st
( Q = SF . i & b2 . i = Intersect Q ) ) holds
b1 = b2
proof end;
end;

:: deftheorem MSSUBFAM:def 1 :
canceled;

:: deftheorem Def2 defines meet MSSUBFAM:def 2 :
for I being set
for M being ManySortedSet of I
for SF being MSSubsetFamily of M
for b4 being ManySortedSet of I holds
( b4 = meet SF iff for i being set st i in I holds
ex Q being Subset-Family of (M . i) st
( Q = SF . i & b4 . i = Intersect Q ) );

definition
let I be set ;
let M be ManySortedSet of I;
let SF be MSSubsetFamily of M;
:: original: meet
redefine func meet SF -> ManySortedSubset of M;
coherence
meet SF is ManySortedSubset of M
proof end;
end;

theorem Th41: :: MSSUBFAM:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for M being ManySortedSet of I
for SF being MSSubsetFamily of M st SF = [0] I holds
meet SF = M
proof end;

theorem :: MSSUBFAM:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for M being ManySortedSet of I
for SFe being V3 MSSubsetFamily of M holds meet SFe c= union SFe
proof end;

theorem :: MSSUBFAM:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for M, A being ManySortedSet of I
for SF being MSSubsetFamily of M st A in SF holds
meet SF c= A
proof end;

theorem :: MSSUBFAM:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for M being ManySortedSet of I
for SF being MSSubsetFamily of M st [0] I in SF holds
meet SF = [0] I
proof end;

theorem :: MSSUBFAM:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for Z, M being ManySortedSet of I
for SF being V3 MSSubsetFamily of M st ( for Z1 being ManySortedSet of I st Z1 in SF holds
Z c= Z1 ) holds
Z c= meet SF
proof end;

theorem :: MSSUBFAM:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for M being ManySortedSet of I
for SF, SG being MSSubsetFamily of M st SF c= SG holds
meet SG c= meet SF
proof end;

theorem :: MSSUBFAM:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for M, A, B being ManySortedSet of I
for SF being MSSubsetFamily of M st A in SF & A c= B holds
meet SF c= B
proof end;

theorem :: MSSUBFAM:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for M, A, B being ManySortedSet of I
for SF being MSSubsetFamily of M st A in SF & A /\ B = [0] I holds
(meet SF) /\ B = [0] I
proof end;

theorem :: MSSUBFAM:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for M being ManySortedSet of I
for SH, SF, SG being MSSubsetFamily of M st SH = SF \/ SG holds
meet SH = (meet SF) /\ (meet SG)
proof end;

theorem :: MSSUBFAM:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for M being ManySortedSet of I
for SF being MSSubsetFamily of M
for V being ManySortedSubset of M st SF = {V} holds
meet SF = V
proof end;

theorem Th51: :: MSSUBFAM:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for M being ManySortedSet of I
for SF being MSSubsetFamily of M
for V, W being ManySortedSubset of M st SF = {V,W} holds
meet SF = V /\ W
proof end;

theorem :: MSSUBFAM:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for M, A being ManySortedSet of I
for SF being MSSubsetFamily of M st A in meet SF holds
for B being ManySortedSet of I st B in SF holds
A in B
proof end;

theorem :: MSSUBFAM:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A, M being ManySortedSet of I
for SF being V3 MSSubsetFamily of M st A in M & ( for B being ManySortedSet of I st B in SF holds
A in B ) holds
A in meet SF
proof end;

definition
let I be set ;
let M be ManySortedSet of I;
let IT be MSSubsetFamily of M;
attr IT is additive means :: MSSUBFAM:def 3
for A, B being ManySortedSet of I st A in IT & B in IT holds
A \/ B in IT;
attr IT is absolutely-additive means :Def4: :: MSSUBFAM:def 4
for F being MSSubsetFamily of M st F c= IT holds
union F in IT;
attr IT is multiplicative means :: MSSUBFAM:def 5
for A, B being ManySortedSet of I st A in IT & B in IT holds
A /\ B in IT;
attr IT is absolutely-multiplicative means :Def6: :: MSSUBFAM:def 6
for F being MSSubsetFamily of M st F c= IT holds
meet F in IT;
attr IT is properly-upper-bound means :Def7: :: MSSUBFAM:def 7
M in IT;
attr IT is properly-lower-bound means :Def8: :: MSSUBFAM:def 8
[0] I in IT;
end;

:: deftheorem defines additive MSSUBFAM:def 3 :
for I being set
for M being ManySortedSet of I
for IT being MSSubsetFamily of M holds
( IT is additive iff for A, B being ManySortedSet of I st A in IT & B in IT holds
A \/ B in IT );

:: deftheorem Def4 defines absolutely-additive MSSUBFAM:def 4 :
for I being set
for M being ManySortedSet of I
for IT being MSSubsetFamily of M holds
( IT is absolutely-additive iff for F being MSSubsetFamily of M st F c= IT holds
union F in IT );

:: deftheorem defines multiplicative MSSUBFAM:def 5 :
for I being set
for M being ManySortedSet of I
for IT being MSSubsetFamily of M holds
( IT is multiplicative iff for A, B being ManySortedSet of I st A in IT & B in IT holds
A /\ B in IT );

:: deftheorem Def6 defines absolutely-multiplicative MSSUBFAM:def 6 :
for I being set
for M being ManySortedSet of I
for IT being MSSubsetFamily of M holds
( IT is absolutely-multiplicative iff for F being MSSubsetFamily of M st F c= IT holds
meet F in IT );

:: deftheorem Def7 defines properly-upper-bound MSSUBFAM:def 7 :
for I being set
for M being ManySortedSet of I
for IT being MSSubsetFamily of M holds
( IT is properly-upper-bound iff M in IT );

:: deftheorem Def8 defines properly-lower-bound MSSUBFAM:def 8 :
for I being set
for M being ManySortedSet of I
for IT being MSSubsetFamily of M holds
( IT is properly-lower-bound iff [0] I in IT );

Lm1: for I being set
for M being ManySortedSet of I holds
( bool M is additive & bool M is absolutely-additive & bool M is multiplicative & bool M is absolutely-multiplicative & bool M is properly-upper-bound & bool M is properly-lower-bound )
proof end;

registration
let I be set ;
let M be ManySortedSet of I;
cluster V3 additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of bool M;
existence
ex b1 being MSSubsetFamily of M st
( b1 is non-empty & b1 is additive & b1 is absolutely-additive & b1 is multiplicative & b1 is absolutely-multiplicative & b1 is properly-upper-bound & b1 is properly-lower-bound )
proof end;
end;

definition
let I be set ;
let M be ManySortedSet of I;
:: original: bool
redefine func bool M -> additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound MSSubsetFamily of M;
coherence
bool M is additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound MSSubsetFamily of M
by Lm1;
end;

registration
let I be set ;
let M be ManySortedSet of I;
cluster absolutely-additive -> additive ManySortedSubset of bool M;
coherence
for b1 being MSSubsetFamily of M st b1 is absolutely-additive holds
b1 is additive
proof end;
end;

registration
let I be set ;
let M be ManySortedSet of I;
cluster absolutely-multiplicative -> multiplicative ManySortedSubset of bool M;
coherence
for b1 being MSSubsetFamily of M st b1 is absolutely-multiplicative holds
b1 is multiplicative
proof end;
end;

registration
let I be set ;
let M be ManySortedSet of I;
cluster absolutely-multiplicative -> properly-upper-bound ManySortedSubset of bool M;
coherence
for b1 being MSSubsetFamily of M st b1 is absolutely-multiplicative holds
b1 is properly-upper-bound
proof end;
end;

registration
let I be set ;
let M be ManySortedSet of I;
cluster properly-upper-bound -> V3 ManySortedSubset of bool M;
coherence
for b1 being MSSubsetFamily of M st b1 is properly-upper-bound holds
b1 is non-empty
proof end;
end;

registration
let I be set ;
let M be ManySortedSet of I;
cluster absolutely-additive -> properly-lower-bound ManySortedSubset of bool M;
coherence
for b1 being MSSubsetFamily of M st b1 is absolutely-additive holds
b1 is properly-lower-bound
proof end;
end;

registration
let I be set ;
let M be ManySortedSet of I;
cluster properly-lower-bound -> V3 ManySortedSubset of bool M;
coherence
for b1 being MSSubsetFamily of M st b1 is properly-lower-bound holds
b1 is non-empty
proof end;
end;