:: by Artur Korni{\l}owicz

::

:: Received October 27, 1995

:: Copyright (c) 1995-2012 Association of Mizar Users

begin

registration

let I be set ;

let F be ManySortedFunction of I;

coherence

doms F is I -defined

rngs F is I -defined

end;
let F be ManySortedFunction of I;

coherence

doms F is I -defined

proof end;

coherence rngs F is I -defined

proof end;

registration

let I be set ;

let F be ManySortedFunction of I;

coherence

for b_{1} being I -defined Function st b_{1} = doms F holds

b_{1} is total

for b_{1} being I -defined Function st b_{1} = rngs F holds

b_{1} is total

end;
let F be ManySortedFunction of I;

coherence

for b

b

proof end;

coherence for b

b

proof end;

scheme :: MSSUBFAM:sch 1

MSFExFunc{ F_{1}() -> set , F_{2}() -> ManySortedSet of F_{1}(), F_{3}() -> ManySortedSet of F_{1}(), P_{1}[ set , set , set ] } :

MSFExFunc{ F

ex F being ManySortedFunction of F_{2}(),F_{3}() st

for i being set st i in F_{1}() holds

ex f being Function of (F_{2}() . i),(F_{3}() . i) st

( f = F . i & ( for x being set st x in F_{2}() . i holds

P_{1}[f . x,x,i] ) )

providedfor i being set st i in F

ex f being Function of (F

( f = F . i & ( for x being set st x in F

P

A1:
for i being set st i in F_{1}() holds

for x being set st x in F_{2}() . i holds

ex y being set st

( y in F_{3}() . i & P_{1}[y,x,i] )

for x being set st x in F

ex y being set st

( y in F

proof end;

theorem :: MSSUBFAM:4

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

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

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

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:7

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

for sf being Subset-Family of I st G in sf & G misses H holds

Intersect sf misses H

proof end;

theorem :: MSSUBFAM:8

for I being set

for sh, sf, sg being Subset-Family of I st sh = sf \/ sg holds

Intersect sh = (Intersect sf) /\ (Intersect sg)

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

for I being set

for sf being Subset-Family of I

for v being Subset of I st sf = {v} holds

Intersect sf = v

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

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

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:12

for I being set

for A being ManySortedSet of I

for B being V8() ManySortedSet of I st A is Element of B holds

A in B

for A being ManySortedSet of I

for B being V8() ManySortedSet of I st A is Element of B holds

A in B

proof end;

theorem Th13: :: MSSUBFAM:13

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

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

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

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:16

for I being set

for A being V8() ManySortedSet of I

for F being ManySortedFunction of A, [[0]] I holds F = [[0]] I

for A being V8() ManySortedSet of I

for F being ManySortedFunction of A, [[0]] I holds F = [[0]] I

proof end;

theorem :: MSSUBFAM:17

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 )

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;

begin

registration

let I be set ;

coherence

for b_{1} being ManySortedSet of I st b_{1} is V9() holds

b_{1} is V36()

end;
coherence

for b

b

proof end;

registration
end;

registration

let I be set ;

let A be ManySortedSet of I;

existence

ex b_{1} being ManySortedSubset of A st

( b_{1} is V9() & b_{1} is V36() )

end;
let A be ManySortedSet of I;

existence

ex b

( b

proof end;

registration

let I be set ;

let A be V36() ManySortedSet of I;

coherence

for b_{1} being ManySortedSubset of A holds b_{1} is V36()

end;
let A be V36() ManySortedSet of I;

coherence

for b

proof end;

registration
end;

registration

let I be set ;

let A be ManySortedSet of I;

let B be V36() ManySortedSet of I;

coherence

A /\ B is finite-yielding

end;
let A be ManySortedSet of I;

let B be V36() ManySortedSet of I;

coherence

A /\ B is finite-yielding

proof end;

registration

let I be set ;

let B be ManySortedSet of I;

let A be V36() ManySortedSet of I;

coherence

A /\ B is finite-yielding ;

end;
let B be ManySortedSet of I;

let A be V36() ManySortedSet of I;

coherence

A /\ B is finite-yielding ;

registration

let I be set ;

let B be ManySortedSet of I;

let A be V36() ManySortedSet of I;

coherence

A \ B is finite-yielding

end;
let B be ManySortedSet of I;

let A be V36() ManySortedSet of I;

coherence

A \ B is finite-yielding

proof end;

registration

let I be set ;

let F be ManySortedFunction of I;

let A be V36() ManySortedSet of I;

coherence

F .:.: A is finite-yielding

end;
let F be ManySortedFunction of I;

let A be V36() ManySortedSet of I;

coherence

F .:.: A is finite-yielding

proof end;

registration
end;

registration
end;

theorem :: MSSUBFAM:22

for I being set

for A being V8() ManySortedSet of I st A is V36() & ( for M being ManySortedSet of I st M in A holds

M is V36() ) holds

union A is V36()

for A being V8() ManySortedSet of I st A is V36() & ( for M being ManySortedSet of I st M in A holds

M is V36() ) holds

union A is V36()

proof end;

theorem :: MSSUBFAM:23

for I being set

for A being ManySortedSet of I st union A is V36() holds

( A is V36() & ( for M being ManySortedSet of I st M in A holds

M is V36() ) )

for A being ManySortedSet of I st union A is V36() holds

( A is V36() & ( for M being ManySortedSet of I st M in A holds

M is V36() ) )

proof end;

theorem :: MSSUBFAM:25

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 V36()

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 V36()

proof end;

registration

let I be set ;

let A, B be V36() ManySortedSet of I;

coherence

(Funcs) (A,B) is finite-yielding

end;
let A, B be V36() ManySortedSet of I;

coherence

(Funcs) (A,B) is finite-yielding

proof end;

registration
end;

theorem :: MSSUBFAM:26

for I being set

for X, Y, Z being ManySortedSet of I st X is V36() & X c= [|Y,Z|] holds

ex A, B being ManySortedSet of I st

( A is V36() & A c= Y & B is V36() & B c= Z & X c= [|A,B|] )

for X, Y, Z being ManySortedSet of I st X is V36() & X c= [|Y,Z|] holds

ex A, B being ManySortedSet of I st

( A is V36() & A c= Y & B is V36() & B c= Z & X c= [|A,B|] )

proof end;

theorem :: MSSUBFAM:27

for I being set

for X, Y, Z being ManySortedSet of I st X is V36() & X c= [|Y,Z|] holds

ex A being ManySortedSet of I st

( A is V36() & A c= Y & X c= [|A,Z|] )

for X, Y, Z being ManySortedSet of I st X is V36() & X c= [|Y,Z|] holds

ex A being ManySortedSet of I st

( A is V36() & A c= Y & X c= [|A,Z|] )

proof end;

theorem :: MSSUBFAM:28

for I being set

for M being V8() V36() 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 ) )

for M being V8() V36() 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

for I being set

for M being V8() V36() 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 ) )

for M being V8() V36() 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

for I being set

for F being ManySortedFunction of I

for Z being ManySortedSet of I st Z is V36() & Z c= rngs F holds

ex Y being ManySortedSet of I st

( Y c= doms F & Y is V36() & F .:.: Y = Z )

for F being ManySortedFunction of I

for Z being ManySortedSet of I st Z is V36() & Z c= rngs F holds

ex Y being ManySortedSet of I st

( Y c= doms F & Y is V36() & F .:.: Y = Z )

proof end;

begin

definition
end;

registration

let I be set ;

let M be ManySortedSet of I;

existence

not for b_{1} being MSSubsetFamily of M holds b_{1} is V8()

end;
let M be ManySortedSet of I;

existence

not for b

proof 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 18;

end;
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 18;

registration

let I be set ;

let M be ManySortedSet of I;

existence

ex b_{1} being MSSubsetFamily of M st

( b_{1} is V9() & b_{1} is V36() )

end;
let M be ManySortedSet of I;

existence

ex b

( b

proof end;

registration

let I be set ;

let M be V36() ManySortedSet of I;

existence

ex b_{1} being MSSubsetFamily of M st

( b_{1} is V8() & b_{1} is V36() )

end;
let M be V36() ManySortedSet of I;

existence

ex b

( b

proof 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)

end;
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;

theorem Th32: :: MSSUBFAM:32

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)

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

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

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

for I being set

for M being ManySortedSet of I

for SF, SG being MSSubsetFamily of M holds SF \/ SG is MSSubsetFamily of M

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

for I being set

for M being ManySortedSet of I

for SF, SG being MSSubsetFamily of M holds SF /\ SG is MSSubsetFamily of M

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

for I being set

for A, M being ManySortedSet of I

for SF being MSSubsetFamily of M holds SF \ A is MSSubsetFamily of M

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

for I being set

for M being ManySortedSet of I

for SF, SG being MSSubsetFamily of M holds SF \+\ SG is MSSubsetFamily of M

for M being ManySortedSet of I

for SF, SG being MSSubsetFamily of M holds SF \+\ SG is MSSubsetFamily of M

proof end;

theorem Th39: :: MSSUBFAM:39

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

for A, M, B being ManySortedSet of I st A c= M & B c= M holds

{A,B} is MSSubsetFamily of M

proof end;

begin

definition

let I be set ;

let M be ManySortedSet of I;

let SF be MSSubsetFamily of M;

ex b_{1} 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 & b_{1} . i = Intersect Q )

for b_{1}, b_{2} 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 & b_{1} . i = Intersect Q ) ) & ( for i being set st i in I holds

ex Q being Subset-Family of (M . i) st

( Q = SF . i & b_{2} . i = Intersect Q ) ) holds

b_{1} = b_{2}

end;
let M be ManySortedSet of I;

let SF be MSSubsetFamily of M;

func meet SF -> ManySortedSet of I means :Def1: :: MSSUBFAM:def 1

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 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 );

ex b

for i being set st i in I holds

ex Q being Subset-Family of (M . i) st

( Q = SF . i & b

proof end;

uniqueness for b

ex Q being Subset-Family of (M . i) st

( Q = SF . i & b

ex Q being Subset-Family of (M . i) st

( Q = SF . i & b

b

proof end;

:: deftheorem Def1 defines meet MSSUBFAM:def 1 :

for I being set

for M being ManySortedSet of I

for SF being MSSubsetFamily of M

for b_{4} being ManySortedSet of I holds

( b_{4} = meet SF iff for i being set st i in I holds

ex Q being Subset-Family of (M . i) st

( Q = SF . i & b_{4} . i = Intersect Q ) );

for I being set

for M being ManySortedSet of I

for SF being MSSubsetFamily of M

for b

( b

ex Q being Subset-Family of (M . i) st

( Q = SF . i & b

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

end;
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;

theorem Th41: :: MSSUBFAM:41

for I being set

for M being ManySortedSet of I

for SF being MSSubsetFamily of M st SF = [[0]] I holds

meet SF = M

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

for I being set

for M being ManySortedSet of I

for SFe being V8() MSSubsetFamily of M holds meet SFe c= union SFe

for M being ManySortedSet of I

for SFe being V8() MSSubsetFamily of M holds meet SFe c= union SFe

proof end;

theorem :: MSSUBFAM:43

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

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

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

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

for I being set

for Z, M being ManySortedSet of I

for SF being V8() MSSubsetFamily of M st ( for Z1 being ManySortedSet of I st Z1 in SF holds

Z c= Z1 ) holds

Z c= meet SF

for Z, M being ManySortedSet of I

for SF being V8() 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

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

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

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

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

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

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

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)

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

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

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

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

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

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

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

for I being set

for A, M being ManySortedSet of I

for SF being V8() 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

for A, M being ManySortedSet of I

for SF being V8() 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;

end;
let M be ManySortedSet of I;

let IT be MSSubsetFamily of M;

attr IT is additive means :: MSSUBFAM:def 2

for A, B being ManySortedSet of I st A in IT & B in IT holds

A \/ B in IT;

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 :Def3: :: MSSUBFAM:def 3

for F being MSSubsetFamily of M st F c= IT holds

union F in IT;

for F being MSSubsetFamily of M st F c= IT holds

union F in IT;

attr IT is multiplicative means :: MSSUBFAM:def 4

for A, B being ManySortedSet of I st A in IT & B in IT holds

A /\ B in IT;

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 :Def5: :: MSSUBFAM:def 5

for F being MSSubsetFamily of M st F c= IT holds

meet F in IT;

for F being MSSubsetFamily of M st F c= IT holds

meet F in IT;

:: deftheorem defines additive MSSUBFAM:def 2 :

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 );

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 Def3 defines absolutely-additive MSSUBFAM:def 3 :

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 );

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 4 :

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 );

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 Def5 defines absolutely-multiplicative MSSUBFAM:def 5 :

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 );

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 Def6 defines properly-upper-bound MSSUBFAM:def 6 :

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 );

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 Def7 defines properly-lower-bound MSSUBFAM:def 7 :

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 );

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;

ex b_{1} being MSSubsetFamily of M st

( b_{1} is V8() & b_{1} is additive & b_{1} is absolutely-additive & b_{1} is multiplicative & b_{1} is absolutely-multiplicative & b_{1} is properly-upper-bound & b_{1} is properly-lower-bound )

end;
let M be ManySortedSet of I;

cluster Relation-like V8() I -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound for ManySortedSubset of bool M;

existence ex b

( b

proof 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;
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;

registration

let I be set ;

let M be ManySortedSet of I;

coherence

for b_{1} being MSSubsetFamily of M st b_{1} is absolutely-additive holds

b_{1} is additive

end;
let M be ManySortedSet of I;

coherence

for b

b

proof end;

registration

let I be set ;

let M be ManySortedSet of I;

coherence

for b_{1} being MSSubsetFamily of M st b_{1} is absolutely-multiplicative holds

b_{1} is multiplicative

end;
let M be ManySortedSet of I;

coherence

for b

b

proof end;

registration

let I be set ;

let M be ManySortedSet of I;

coherence

for b_{1} being MSSubsetFamily of M st b_{1} is absolutely-multiplicative holds

b_{1} is properly-upper-bound

end;
let M be ManySortedSet of I;

coherence

for b

b

proof end;

registration

let I be set ;

let M be ManySortedSet of I;

coherence

for b_{1} being MSSubsetFamily of M st b_{1} is properly-upper-bound holds

b_{1} is V8()

end;
let M be ManySortedSet of I;

coherence

for b

b

proof end;

registration

let I be set ;

let M be ManySortedSet of I;

coherence

for b_{1} being MSSubsetFamily of M st b_{1} is absolutely-additive holds

b_{1} is properly-lower-bound

end;
let M be ManySortedSet of I;

coherence

for b

b

proof end;

registration

let I be set ;

let M be ManySortedSet of I;

coherence

for b_{1} being MSSubsetFamily of M st b_{1} is properly-lower-bound holds

b_{1} is V8()

end;
let M be ManySortedSet of I;

coherence

for b

b

proof end;