begin
Lm1:
for I, i being set
for A being V30() ManySortedSet of I st i in I holds
A . i is finite
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th13:
theorem Th14:
theorem
theorem
theorem
begin
theorem Th18:
theorem
theorem
theorem Th21:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
begin
theorem
theorem Th32:
theorem Th33:
theorem Th34:
theorem
theorem Th36:
theorem
theorem Th38:
theorem Th39:
theorem Th40:
begin
:: deftheorem MSSUBFAM:def 1 :
canceled;
:: deftheorem Def2 defines meet MSSUBFAM:def 2 :
theorem Th41:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th51:
theorem
theorem
:: deftheorem defines additive MSSUBFAM:def 3 :
:: deftheorem Def4 defines absolutely-additive MSSUBFAM:def 4 :
:: deftheorem defines multiplicative MSSUBFAM:def 5 :
:: deftheorem Def6 defines absolutely-multiplicative MSSUBFAM:def 6 :
:: deftheorem Def7 defines properly-upper-bound MSSUBFAM:def 7 :
:: deftheorem Def8 defines properly-lower-bound MSSUBFAM:def 8 :
Lm2:
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 )