:: by Mariusz Giero

::

:: Received December 28, 2001

:: Copyright (c) 2001-2021 Association of Mizar Users

definition

let A be RelStr ;

end;
attr A is with_superior means :: TAXONOM2:def 1

ex x being Element of A st x is_superior_of the InternalRel of A;

ex x being Element of A st x is_superior_of the InternalRel of A;

:: deftheorem defines with_superior TAXONOM2:def 1 :

for A being RelStr holds

( A is with_superior iff ex x being Element of A st x is_superior_of the InternalRel of A );

for A being RelStr holds

( A is with_superior iff ex x being Element of A st x is_superior_of the InternalRel of A );

definition

let A be RelStr ;

end;
attr A is with_comparable_down means :Def2: :: TAXONOM2:def 2

for x, y being Element of A holds

( for z being Element of A holds

( not z <= x or not z <= y ) or x <= y or y <= x );

for x, y being Element of A holds

( for z being Element of A holds

( not z <= x or not z <= y ) or x <= y or y <= x );

:: deftheorem Def2 defines with_comparable_down TAXONOM2:def 2 :

for A being RelStr holds

( A is with_comparable_down iff for x, y being Element of A holds

( for z being Element of A holds

( not z <= x or not z <= y ) or x <= y or y <= x ) );

for A being RelStr holds

( A is with_comparable_down iff for x, y being Element of A holds

( for z being Element of A holds

( not z <= x or not z <= y ) or x <= y or y <= x ) );

theorem Th1: :: TAXONOM2:1

for a being set holds

( not InclPoset {{a}} is empty & InclPoset {{a}} is reflexive & InclPoset {{a}} is transitive & InclPoset {{a}} is antisymmetric & InclPoset {{a}} is with_superior & InclPoset {{a}} is with_comparable_down )

( not InclPoset {{a}} is empty & InclPoset {{a}} is reflexive & InclPoset {{a}} is transitive & InclPoset {{a}} is antisymmetric & InclPoset {{a}} is with_superior & InclPoset {{a}} is with_comparable_down )

proof end;

registration

ex b_{1} being RelStr st

( not b_{1} is empty & b_{1} is reflexive & b_{1} is transitive & b_{1} is antisymmetric & b_{1} is with_superior & b_{1} is with_comparable_down & b_{1} is strict )
end;

cluster non empty strict reflexive transitive antisymmetric with_superior with_comparable_down for RelStr ;

existence ex b

( not b

proof end;

theorem :: TAXONOM2:2

for X being non empty set

for EqR being Equivalence_Relation of X

for x, y, z being set st z in Class (EqR,x) & z in Class (EqR,y) holds

Class (EqR,x) = Class (EqR,y)

for EqR being Equivalence_Relation of X

for x, y, z being set st z in Class (EqR,x) & z in Class (EqR,y) holds

Class (EqR,x) = Class (EqR,y)

proof end;

Lm1: for X being non empty set

for P being a_partition of X

for x, y, z being set st x in P & y in P & z in x & z in y holds

x = y

by EQREL_1:70;

theorem Th3: :: TAXONOM2:4

for X being non empty set

for C, x being set st C is Classification of X & x in union C holds

x c= X

for C, x being set st C is Classification of X & x in union C holds

x c= X

proof end;

theorem :: TAXONOM2:5

for X being non empty set

for C being set st C is Strong_Classification of X holds

InclPoset (union C) is Tree

for C being set st C is Strong_Classification of X holds

InclPoset (union C) is Tree

proof end;

definition

let Y be set ;

end;
attr Y is hierarchic means :: TAXONOM2:def 3

for x, y being set st x in Y & y in Y & not x c= y & not y c= x holds

x misses y;

for x, y being set st x in Y & y in Y & not x c= y & not y c= x holds

x misses y;

:: deftheorem defines hierarchic TAXONOM2:def 3 :

for Y being set holds

( Y is hierarchic iff for x, y being set st x in Y & y in Y & not x c= y & not y c= x holds

x misses y );

for Y being set holds

( Y is hierarchic iff for x, y being set st x in Y & y in Y & not x c= y & not y c= x holds

x misses y );

registration
end;

registration
end;

definition
end;

:: deftheorem Def4 defines Hierarchy TAXONOM2:def 4 :

for Y being set

for b_{2} being Subset-Family of Y holds

( b_{2} is Hierarchy of Y iff b_{2} is hierarchic );

for Y being set

for b

( b

definition

let Y be set ;

end;
attr Y is mutually-disjoint means :Def5: :: TAXONOM2:def 5

for x, y being set st x in Y & y in Y & x <> y holds

x misses y;

for x, y being set st x in Y & y in Y & x <> y holds

x misses y;

:: deftheorem Def5 defines mutually-disjoint TAXONOM2:def 5 :

for Y being set holds

( Y is mutually-disjoint iff for x, y being set st x in Y & y in Y & x <> y holds

x misses y );

for Y being set holds

( Y is mutually-disjoint iff for x, y being set st x in Y & y in Y & x <> y holds

x misses y );

Lm2: now :: thesis: for x, y being set st x in {{}} & y in {{}} & x <> y holds

x misses y

x misses y

let x, y be set ; :: thesis: ( x in {{}} & y in {{}} & x <> y implies x misses y )

assume that

A1: x in {{}} and

A2: y in {{}} and

A3: x <> y ; :: thesis: x misses y

x = {} by A1, TARSKI:def 1;

hence x misses y by A2, A3, TARSKI:def 1; :: thesis: verum

end;
assume that

A1: x in {{}} and

A2: y in {{}} and

A3: x <> y ; :: thesis: x misses y

x = {} by A1, TARSKI:def 1;

hence x misses y by A2, A3, TARSKI:def 1; :: thesis: verum

registration
end;

Lm3: now :: thesis: for Y being set

for H being Hierarchy of Y st H is covering holds

for B being mutually-disjoint Subset-Family of Y st B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds

B = C ) holds

union B = Y

for H being Hierarchy of Y st H is covering holds

for B being mutually-disjoint Subset-Family of Y st B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds

B = C ) holds

union B = Y

let Y be set ; :: thesis: for H being Hierarchy of Y st H is covering holds

for B being mutually-disjoint Subset-Family of Y st B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds

B = C ) holds

union B = Y

let H be Hierarchy of Y; :: thesis: ( H is covering implies for B being mutually-disjoint Subset-Family of Y st B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds

B = C ) holds

union B = Y )

assume A1: H is covering ; :: thesis: for B being mutually-disjoint Subset-Family of Y st B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds

B = C ) holds

union B = Y

let B be mutually-disjoint Subset-Family of Y; :: thesis: ( B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds

B = C ) implies union B = Y )

assume that

A2: B c= H and

A3: for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds

B = C ; :: thesis: union B = Y

Y c= union B

end;
for B being mutually-disjoint Subset-Family of Y st B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds

B = C ) holds

union B = Y

let H be Hierarchy of Y; :: thesis: ( H is covering implies for B being mutually-disjoint Subset-Family of Y st B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds

B = C ) holds

union B = Y )

assume A1: H is covering ; :: thesis: for B being mutually-disjoint Subset-Family of Y st B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds

B = C ) holds

union B = Y

let B be mutually-disjoint Subset-Family of Y; :: thesis: ( B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds

B = C ) implies union B = Y )

assume that

A2: B c= H and

A3: for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds

B = C ; :: thesis: union B = Y

Y c= union B

proof

hence
union B = Y
by XBOOLE_0:def 10; :: thesis: verum
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Y or y in union B )

assume y in Y ; :: thesis: y in union B

then y in union H by A1, ABIAN:4;

then consider x being set such that

A4: y in x and

A5: x in H by TARSKI:def 4;

end;
assume y in Y ; :: thesis: y in union B

then y in union H by A1, ABIAN:4;

then consider x being set such that

A4: y in x and

A5: x in H by TARSKI:def 4;

now :: thesis: y in union B

hence
y in union B
; :: thesis: verum
defpred S_{1}[ set ] means $1 c= x;

consider D being set such that

A6: for a being set holds

( a in D iff ( a in B & S_{1}[a] ) )
from XFAMILY:sch 1();

set C = (B \ D) \/ {x};

A7: B \ D c= (B \ D) \/ {x} by XBOOLE_1:7;

A8: {x} c= H by A5, TARSKI:def 1;

assume A9: not y in union B ; :: thesis: contradiction

A10: for p being set st p in B & not p in D & p <> x holds

p misses x

p misses q

then A25: x in (B \ D) \/ {x} by XBOOLE_0:def 3;

A26: union B c= union ((B \ D) \/ {x})

B \ D c= B by XBOOLE_1:36;

then A30: B \ D c= H by A2;

then (B \ D) \/ {x} c= H by A8, XBOOLE_1:8;

then (B \ D) \/ {x} is mutually-disjoint Subset-Family of Y by A15, Def5, XBOOLE_1:1;

then A31: B = (B \ D) \/ {x} by A3, A30, A8, A26, XBOOLE_1:8;

{x} c= (B \ D) \/ {x} by XBOOLE_1:7;

hence contradiction by A4, A9, A31, A29, TARSKI:def 4; :: thesis: verum

end;
consider D being set such that

A6: for a being set holds

( a in D iff ( a in B & S

set C = (B \ D) \/ {x};

A7: B \ D c= (B \ D) \/ {x} by XBOOLE_1:7;

A8: {x} c= H by A5, TARSKI:def 1;

assume A9: not y in union B ; :: thesis: contradiction

A10: for p being set st p in B & not p in D & p <> x holds

p misses x

proof

A15:
for p, q being set st p in (B \ D) \/ {x} & q in (B \ D) \/ {x} & p <> q holds
A11:
H is hierarchic
by Def4;

let p be set ; :: thesis: ( p in B & not p in D & p <> x implies p misses x )

assume that

A12: p in B and

A13: not p in D and

p <> x ; :: thesis: p misses x

A14: not x c= p by A4, A9, A12, TARSKI:def 4;

not p c= x by A6, A12, A13;

hence p misses x by A2, A5, A12, A14, A11; :: thesis: verum

end;
let p be set ; :: thesis: ( p in B & not p in D & p <> x implies p misses x )

assume that

A12: p in B and

A13: not p in D and

p <> x ; :: thesis: p misses x

A14: not x c= p by A4, A9, A12, TARSKI:def 4;

not p c= x by A6, A12, A13;

hence p misses x by A2, A5, A12, A14, A11; :: thesis: verum

p misses q

proof

x in {x}
by TARSKI:def 1;
let p, q be set ; :: thesis: ( p in (B \ D) \/ {x} & q in (B \ D) \/ {x} & p <> q implies p misses q )

assume that

A16: p in (B \ D) \/ {x} and

A17: q in (B \ D) \/ {x} and

A18: p <> q ; :: thesis: p misses q

end;
assume that

A16: p in (B \ D) \/ {x} and

A17: q in (B \ D) \/ {x} and

A18: p <> q ; :: thesis: p misses q

per cases
( p in B \ D or p in {x} )
by A16, XBOOLE_0:def 3;

end;

suppose A19:
p in B \ D
; :: thesis: p misses q

then A20:
not p in D
by XBOOLE_0:def 5;

A21: p in B by A19, XBOOLE_0:def 5;

end;
A21: p in B by A19, XBOOLE_0:def 5;

suppose
p in {x}
; :: thesis: p misses q

then A22:
p = x
by TARSKI:def 1;

end;
then A25: x in (B \ D) \/ {x} by XBOOLE_0:def 3;

A26: union B c= union ((B \ D) \/ {x})

proof

A29:
x in {x}
by TARSKI:def 1;
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in union B or s in union ((B \ D) \/ {x}) )

assume s in union B ; :: thesis: s in union ((B \ D) \/ {x})

then consider t being set such that

A27: s in t and

A28: t in B by TARSKI:def 4;

end;
assume s in union B ; :: thesis: s in union ((B \ D) \/ {x})

then consider t being set such that

A27: s in t and

A28: t in B by TARSKI:def 4;

B \ D c= B by XBOOLE_1:36;

then A30: B \ D c= H by A2;

then (B \ D) \/ {x} c= H by A8, XBOOLE_1:8;

then (B \ D) \/ {x} is mutually-disjoint Subset-Family of Y by A15, Def5, XBOOLE_1:1;

then A31: B = (B \ D) \/ {x} by A3, A30, A8, A26, XBOOLE_1:8;

{x} c= (B \ D) \/ {x} by XBOOLE_1:7;

hence contradiction by A4, A9, A31, A29, TARSKI:def 4; :: thesis: verum

Lm4: now :: thesis: for Y being set

for H being Hierarchy of Y

for B being mutually-disjoint Subset-Family of Y st B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds

B = C ) holds

for S1 being Subset of Y st S1 in B holds

S1 <> {}

for H being Hierarchy of Y

for B being mutually-disjoint Subset-Family of Y st B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds

B = C ) holds

for S1 being Subset of Y st S1 in B holds

S1 <> {}

let Y be set ; :: thesis: for H being Hierarchy of Y

for B being mutually-disjoint Subset-Family of Y st B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds

B = C ) holds

for S1 being Subset of Y st S1 in B holds

S1 <> {}

let H be Hierarchy of Y; :: thesis: for B being mutually-disjoint Subset-Family of Y st B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds

B = C ) holds

for S1 being Subset of Y st S1 in B holds

S1 <> {}

let B be mutually-disjoint Subset-Family of Y; :: thesis: ( B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds

B = C ) implies for S1 being Subset of Y st S1 in B holds

S1 <> {} )

assume that

A1: B c= H and

A2: for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds

B = C ; :: thesis: for S1 being Subset of Y st S1 in B holds

S1 <> {}

let S1 be Subset of Y; :: thesis: ( S1 in B implies S1 <> {} )

assume A3: S1 in B ; :: thesis: S1 <> {}

end;
for B being mutually-disjoint Subset-Family of Y st B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds

B = C ) holds

for S1 being Subset of Y st S1 in B holds

S1 <> {}

let H be Hierarchy of Y; :: thesis: for B being mutually-disjoint Subset-Family of Y st B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds

B = C ) holds

for S1 being Subset of Y st S1 in B holds

S1 <> {}

let B be mutually-disjoint Subset-Family of Y; :: thesis: ( B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds

B = C ) implies for S1 being Subset of Y st S1 in B holds

S1 <> {} )

assume that

A1: B c= H and

A2: for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds

B = C ; :: thesis: for S1 being Subset of Y st S1 in B holds

S1 <> {}

let S1 be Subset of Y; :: thesis: ( S1 in B implies S1 <> {} )

assume A3: S1 in B ; :: thesis: S1 <> {}

now :: thesis: not S1 = {}

hence
S1 <> {}
; :: thesis: verum
set C = B \ {{}};

assume A4: S1 = {} ; :: thesis: contradiction

A5: union B c= union (B \ {{}})

then B \ {{}} c= H by A1;

then B = B \ {{}} by A2, A5, A8;

then not {} in {{}} by A3, A4, XBOOLE_0:def 5;

hence contradiction by TARSKI:def 1; :: thesis: verum

end;
assume A4: S1 = {} ; :: thesis: contradiction

A5: union B c= union (B \ {{}})

proof

A8:
B \ {{}} is mutually-disjoint
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union B or x in union (B \ {{}}) )

assume x in union B ; :: thesis: x in union (B \ {{}})

then consider y being set such that

A6: x in y and

A7: y in B by TARSKI:def 4;

not y in {{}} by A6, TARSKI:def 1;

then y in B \ {{}} by A7, XBOOLE_0:def 5;

hence x in union (B \ {{}}) by A6, TARSKI:def 4; :: thesis: verum

end;
assume x in union B ; :: thesis: x in union (B \ {{}})

then consider y being set such that

A6: x in y and

A7: y in B by TARSKI:def 4;

not y in {{}} by A6, TARSKI:def 1;

then y in B \ {{}} by A7, XBOOLE_0:def 5;

hence x in union (B \ {{}}) by A6, TARSKI:def 4; :: thesis: verum

proof

B \ {{}} c= B
by XBOOLE_1:36;
let x, y be set ; :: according to TAXONOM2:def 5 :: thesis: ( x in B \ {{}} & y in B \ {{}} & x <> y implies x misses y )

assume that

A9: x in B \ {{}} and

A10: y in B \ {{}} and

A11: x <> y ; :: thesis: x misses y

A12: y in B by A10, XBOOLE_0:def 5;

x in B by A9, XBOOLE_0:def 5;

hence x misses y by A11, A12, Def5; :: thesis: verum

end;
assume that

A9: x in B \ {{}} and

A10: y in B \ {{}} and

A11: x <> y ; :: thesis: x misses y

A12: y in B by A10, XBOOLE_0:def 5;

x in B by A9, XBOOLE_0:def 5;

hence x misses y by A11, A12, Def5; :: thesis: verum

then B \ {{}} c= H by A1;

then B = B \ {{}} by A2, A5, A8;

then not {} in {{}} by A3, A4, XBOOLE_0:def 5;

hence contradiction by TARSKI:def 1; :: thesis: verum

:: deftheorem Def6 defines T_3 TAXONOM2:def 6 :

for Y being set

for F being Subset-Family of Y holds

( F is T_3 iff for A being Subset of Y st A in F holds

for x being Element of Y st not x in A holds

ex B being Subset of Y st

( x in B & B in F & A misses B ) );

for Y being set

for F being Subset-Family of Y holds

( F is T_3 iff for A being Subset of Y st A in F holds

for x being Element of Y st not x in A holds

ex B being Subset of Y st

( x in B & B in F & A misses B ) );

registration

let Y be set ;

existence

ex b_{1} being Hierarchy of Y st

( b_{1} is covering & b_{1} is T_3 )

end;
existence

ex b

( b

proof end;

:: deftheorem defines lower-bounded TAXONOM2:def 7 :

for Y being set

for F being Subset-Family of Y holds

( F is lower-bounded iff for B being set st B <> {} & B c= F & B is c=-linear holds

ex c being set st

( c in F & c c= meet B ) );

for Y being set

for F being Subset-Family of Y holds

( F is lower-bounded iff for B being set st B <> {} & B c= F & B is c=-linear holds

ex c being set st

( c in F & c c= meet B ) );

theorem Th11: :: TAXONOM2:12

for Y being set

for S1 being Subset of Y

for B being mutually-disjoint Subset-Family of Y st ( for b being set st b in B holds

( S1 misses b & Y <> {} ) ) holds

( B \/ {S1} is mutually-disjoint Subset-Family of Y & ( S1 <> {} implies union (B \/ {S1}) <> union B ) )

for S1 being Subset of Y

for B being mutually-disjoint Subset-Family of Y st ( for b being set st b in B holds

( S1 misses b & Y <> {} ) ) holds

( B \/ {S1} is mutually-disjoint Subset-Family of Y & ( S1 <> {} implies union (B \/ {S1}) <> union B ) )

proof end;

:: deftheorem defines with_max's TAXONOM2:def 8 :

for Y being set

for F being Subset-Family of Y holds

( F is with_max's iff for S being Subset of Y st S in F holds

ex T being Subset of Y st

( S c= T & T in F & ( for V being Subset of Y st T c= V & V in F holds

V = Y ) ) );

for Y being set

for F being Subset-Family of Y holds

( F is with_max's iff for S being Subset of Y st S in F holds

ex T being Subset of Y st

( S c= T & T in F & ( for V being Subset of Y st T c= V & V in F holds

V = Y ) ) );

theorem :: TAXONOM2:13

for Y being set

for H being covering Hierarchy of Y st H is with_max's holds

ex P being a_partition of Y st P c= H

for H being covering Hierarchy of Y st H is with_max's holds

ex P being a_partition of Y st P c= H

proof end;

theorem :: TAXONOM2:14

for Y being set

for H being covering Hierarchy of Y

for B being mutually-disjoint Subset-Family of Y st B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds

B = C ) holds

B is a_partition of Y

for H being covering Hierarchy of Y

for B being mutually-disjoint Subset-Family of Y st B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds

B = C ) holds

B is a_partition of Y

proof end;

theorem :: TAXONOM2:15

for Y being set

for H being covering T_3 Hierarchy of Y st H is lower-bounded & not {} in H holds

for A being Subset of Y

for B being mutually-disjoint Subset-Family of Y st A in B & B c= H & ( for C being mutually-disjoint Subset-Family of Y st A in C & C c= H & union B c= union C holds

union B = union C ) holds

B is a_partition of Y

for H being covering T_3 Hierarchy of Y st H is lower-bounded & not {} in H holds

for A being Subset of Y

for B being mutually-disjoint Subset-Family of Y st A in B & B c= H & ( for C being mutually-disjoint Subset-Family of Y st A in C & C c= H & union B c= union C holds

union B = union C ) holds

B is a_partition of Y

proof end;

theorem Th15: :: TAXONOM2:16

for Y being set

for H being covering T_3 Hierarchy of Y st H is lower-bounded & not {} in H holds

for A being Subset of Y

for B being mutually-disjoint Subset-Family of Y st A in B & B c= H & ( for C being mutually-disjoint Subset-Family of Y st A in C & C c= H & B c= C holds

B = C ) holds

B is a_partition of Y

for H being covering T_3 Hierarchy of Y st H is lower-bounded & not {} in H holds

for A being Subset of Y

for B being mutually-disjoint Subset-Family of Y st A in B & B c= H & ( for C being mutually-disjoint Subset-Family of Y st A in C & C c= H & B c= C holds

B = C ) holds

B is a_partition of Y

proof end;

theorem Th16: :: TAXONOM2:17

for Y being set

for H being covering T_3 Hierarchy of Y st H is lower-bounded & not {} in H holds

for A being Subset of Y st A in H holds

ex P being a_partition of Y st

( A in P & P c= H )

for H being covering T_3 Hierarchy of Y st H is lower-bounded & not {} in H holds

for A being Subset of Y st A in H holds

ex P being a_partition of Y st

( A in P & P c= H )

proof end;

Lm5: now :: thesis: for x being non empty set

for y being set st x c= y holds

x meets y

for y being set st x c= y holds

x meets y

let x be non empty set ; :: thesis: for y being set st x c= y holds

x meets y

A1: ex a being object st a in x by XBOOLE_0:def 1;

let y be set ; :: thesis: ( x c= y implies x meets y )

assume x c= y ; :: thesis: x meets y

hence x meets y by A1, XBOOLE_0:3; :: thesis: verum

end;
x meets y

A1: ex a being object st a in x by XBOOLE_0:def 1;

let y be set ; :: thesis: ( x c= y implies x meets y )

assume x c= y ; :: thesis: x meets y

hence x meets y by A1, XBOOLE_0:3; :: thesis: verum

theorem Th17: :: TAXONOM2:18

for X, h being non empty set

for Pmin being a_partition of X

for hw being set st hw in Pmin & h c= hw holds

for PS being a_partition of X st h in PS & ( for x being set holds

( not x in PS or x c= hw or hw c= x or hw misses x ) ) holds

for PT being set st ( for a being set holds

( a in PT iff ( a in PS & a c= hw ) ) ) holds

( PT \/ (Pmin \ {hw}) is a_partition of X & PT \/ (Pmin \ {hw}) is_finer_than Pmin )

for Pmin being a_partition of X

for hw being set st hw in Pmin & h c= hw holds

for PS being a_partition of X st h in PS & ( for x being set holds

( not x in PS or x c= hw or hw c= x or hw misses x ) ) holds

for PT being set st ( for a being set holds

( a in PT iff ( a in PS & a c= hw ) ) ) holds

( PT \/ (Pmin \ {hw}) is a_partition of X & PT \/ (Pmin \ {hw}) is_finer_than Pmin )

proof end;

theorem Th18: :: TAXONOM2:19

for X, h being non empty set st h c= X holds

for Pmax being a_partition of X st ex hy being set st

( hy in Pmax & hy c= h ) & ( for x being set holds

( not x in Pmax or x c= h or h c= x or h misses x ) ) holds

for Pb being set st ( for x being set holds

( x in Pb iff ( x in Pmax & x misses h ) ) ) holds

( Pb \/ {h} is a_partition of X & Pmax is_finer_than Pb \/ {h} & ( for Pmin being a_partition of X st Pmax is_finer_than Pmin holds

for hw being set st hw in Pmin & h c= hw holds

Pb \/ {h} is_finer_than Pmin ) )

for Pmax being a_partition of X st ex hy being set st

( hy in Pmax & hy c= h ) & ( for x being set holds

( not x in Pmax or x c= h or h c= x or h misses x ) ) holds

for Pb being set st ( for x being set holds

( x in Pb iff ( x in Pmax & x misses h ) ) ) holds

( Pb \/ {h} is a_partition of X & Pmax is_finer_than Pb \/ {h} & ( for Pmin being a_partition of X st Pmax is_finer_than Pmin holds

for hw being set st hw in Pmin & h c= hw holds

Pb \/ {h} is_finer_than Pmin ) )

proof end;

theorem :: TAXONOM2:20

for X being non empty set

for H being covering T_3 Hierarchy of X st H is lower-bounded & not {} in H & ( for C1 being set st C1 <> {} & C1 c= PARTITIONS X & ( for P1, P2 being set st P1 in C1 & P2 in C1 & not P1 is_finer_than P2 holds

P2 is_finer_than P1 ) holds

ex PX, PY being set st

( PX in C1 & PY in C1 & ( for PZ being set st PZ in C1 holds

( PZ is_finer_than PY & PX is_finer_than PZ ) ) ) ) holds

ex C being Classification of X st union C = H

for H being covering T_3 Hierarchy of X st H is lower-bounded & not {} in H & ( for C1 being set st C1 <> {} & C1 c= PARTITIONS X & ( for P1, P2 being set st P1 in C1 & P2 in C1 & not P1 is_finer_than P2 holds

P2 is_finer_than P1 ) holds

ex PX, PY being set st

( PX in C1 & PY in C1 & ( for PZ being set st PZ in C1 holds

( PZ is_finer_than PY & PX is_finer_than PZ ) ) ) ) holds

ex C being Classification of X st union C = H

proof end;