:: TAXONOM2 semantic presentation

definition
let c1 be RelStr ;
attr a1 is with_superior means :: TAXONOM2:def 1
ex b1 being Element of a1 st b1 is_superior_of the InternalRel of a1;
end;

:: deftheorem Def1 defines with_superior TAXONOM2:def 1 :
for b1 being RelStr holds
( b1 is with_superior iff ex b2 being Element of b1 st b2 is_superior_of the InternalRel of b1 );

definition
let c1 be RelStr ;
attr a1 is with_comparable_down means :Def2: :: TAXONOM2:def 2
for b1, b2 being Element of a1 holds
( for b3 being Element of a1 holds
( not b3 <= b1 or not b3 <= b2 ) or b1 <= b2 or b2 <= b1 );
end;

:: deftheorem Def2 defines with_comparable_down TAXONOM2:def 2 :
for b1 being RelStr holds
( b1 is with_comparable_down iff for b2, b3 being Element of b1 holds
( for b4 being Element of b1 holds
( not b4 <= b2 or not b4 <= b3 ) or b2 <= b3 or b3 <= b2 ) );

theorem Th1: :: TAXONOM2:1
for b1 being set holds
( not InclPoset {{b1}} is empty & InclPoset {{b1}} is reflexive & InclPoset {{b1}} is transitive & InclPoset {{b1}} is antisymmetric & InclPoset {{b1}} is with_superior & InclPoset {{b1}} is with_comparable_down )
proof end;

registration
cluster non empty strict reflexive transitive antisymmetric with_superior with_comparable_down RelStr ;
existence
ex b1 being RelStr st
( not b1 is empty & b1 is reflexive & b1 is transitive & b1 is antisymmetric & b1 is with_superior & b1 is with_comparable_down & b1 is strict )
proof end;
end;

definition
mode Tree is with_superior with_comparable_down Poset;
end;

theorem Th2: :: TAXONOM2:2
for b1 being non empty set
for b2 being Equivalence_Relation of b1
for b3, b4, b5 being set st b5 in Class b2,b3 & b5 in Class b2,b4 holds
Class b2,b3 = Class b2,b4
proof end;

theorem Th3: :: TAXONOM2:3
for b1 being non empty set
for b2 being a_partition of b1
for b3, b4, b5 being set st b3 in b2 & b4 in b2 & b5 in b3 & b5 in b4 holds
b3 = b4
proof end;

theorem Th4: :: TAXONOM2:4
for b1 being non empty set
for b2, b3 being set st b2 is Classification of b1 & b3 in union b2 holds
b3 c= b1
proof end;

theorem Th5: :: TAXONOM2:5
for b1 being non empty set
for b2 being set st b2 is Strong_Classification of b1 holds
InclPoset (union b2) is Tree
proof end;

definition
let c1 be set ;
attr a1 is hierarchic means :Def3: :: TAXONOM2:def 3
for b1, b2 being set st b1 in a1 & b2 in a1 & not b1 c= b2 & not b2 c= b1 holds
b1 misses b2;
end;

:: deftheorem Def3 defines hierarchic TAXONOM2:def 3 :
for b1 being set holds
( b1 is hierarchic iff for b2, b3 being set st b2 in b1 & b3 in b1 & not b2 c= b3 & not b3 c= b2 holds
b2 misses b3 );

registration
cluster trivial -> hierarchic set ;
coherence
for b1 being set st b1 is trivial holds
b1 is hierarchic
proof end;
end;

registration
cluster non trivial hierarchic set ;
existence
ex b1 being set st
( not b1 is trivial & b1 is hierarchic )
proof end;
end;

theorem Th6: :: TAXONOM2:6
{} is hierarchic
proof end;

theorem Th7: :: TAXONOM2:7
{{} } is hierarchic
proof end;

definition
let c1 be set ;
mode Hierarchy of c1 -> Subset-Family of a1 means :Def4: :: TAXONOM2:def 4
a2 is hierarchic;
existence
ex b1 being Subset-Family of c1 st b1 is hierarchic
proof end;
end;

:: deftheorem Def4 defines Hierarchy TAXONOM2:def 4 :
for b1 being set
for b2 being Subset-Family of b1 holds
( b2 is Hierarchy of b1 iff b2 is hierarchic );

definition
let c1 be set ;
attr a1 is mutually-disjoint means :Def5: :: TAXONOM2:def 5
for b1, b2 being set st b1 in a1 & b2 in a1 & b1 <> b2 holds
b1 misses b2;
end;

:: deftheorem Def5 defines mutually-disjoint TAXONOM2:def 5 :
for b1 being set holds
( b1 is mutually-disjoint iff for b2, b3 being set st b2 in b1 & b3 in b1 & b2 <> b3 holds
b2 misses b3 );

E10: now
let c1, c2 be set ;
assume E11: ( c1 in {{} } & c2 in {{} } & c1 <> c2 ) ;
( c1 = {} & c2 = {} ) by E11, TARSKI:def 1;
hence c1 misses c2 by E11;
end;

registration
let c1 be set ;
cluster mutually-disjoint Element of bool (bool a1);
existence
ex b1 being Subset-Family of c1 st b1 is mutually-disjoint
proof end;
end;

theorem Th8: :: TAXONOM2:8
{} is mutually-disjoint
proof end;

theorem Th9: :: TAXONOM2:9
{{} } is mutually-disjoint by Def5, Lemma10;

theorem Th10: :: TAXONOM2:10
for b1 being set holds {b1} is mutually-disjoint
proof end;

E12: now
let c1 be set ;
let c2 be Hierarchy of c1;
assume E13: c2 is covering ;
let c3 be mutually-disjoint Subset-Family of c1;
assume E14: ( c3 c= c2 & ( for b1 being mutually-disjoint Subset-Family of c1 st b1 c= c2 & union c3 c= union b1 holds
c3 = b1 ) ) ;
thus union c3 = c1
proof
thus union c3 c= c1 ; :: according to XBOOLE_0:def 10
thus c1 c= union c3
proof
let c4 be set ; :: according to TARSKI:def 3
assume E15: c4 in c1 ;
c4 in union c2 by E13, E15, ABIAN:4;
then consider c5 being set such that
E16: ( c4 in c5 & c5 in c2 ) by TARSKI:def 4;
now
assume E17: not c4 in union c3 ;
defpred S1[ set ] means a1 c= c5;
consider c6 being set such that
E18: for b1 being set holds
( b1 in c6 iff ( b1 in c3 & S1[b1] ) ) from XBOOLE_0:sch 1();
set c7 = (c3 \ c6) \/ {c5};
c5 in {c5} by TARSKI:def 1;
then E19: c5 in (c3 \ c6) \/ {c5} by XBOOLE_0:def 2;
E20: c3 \ c6 c= (c3 \ c6) \/ {c5} by XBOOLE_1:7;
c3 \ c6 c= c3 by XBOOLE_1:36;
then E21: c3 \ c6 c= c2 by E14, XBOOLE_1:1;
{c5} c= c2
proof
let c8 be set ; :: according to TARSKI:def 3
assume E22: c8 in {c5} ;
thus c8 in c2 by E16, E22, TARSKI:def 1;
end;
then E22: (c3 \ c6) \/ {c5} c= c2 by E21, XBOOLE_1:8;
then E23: (c3 \ c6) \/ {c5} c= bool c1 by XBOOLE_1:1;
E24: for b1 being set st b1 in c3 & not b1 in c6 & b1 <> c5 holds
b1 misses c5
proof
let c8 be set ;
assume E25: ( c8 in c3 & not c8 in c6 & c8 <> c5 ) ;
E26: not c8 c= c5 by E18, E25;
E27: not c5 c= c8 by E16, E17, E25, TARSKI:def 4;
c2 is hierarchic by Def4;
hence c8 misses c5 by E14, E16, E25, E26, E27, Def3;
end;
for b1, b2 being set st b1 in (c3 \ c6) \/ {c5} & b2 in (c3 \ c6) \/ {c5} & b1 <> b2 holds
b1 misses b2
proof
let c8, c9 be set ;
assume E25: ( c8 in (c3 \ c6) \/ {c5} & c9 in (c3 \ c6) \/ {c5} & c8 <> c9 ) ;
per cases ( c8 in c3 \ c6 or c8 in {c5} ) by E25, XBOOLE_0:def 2;
suppose c8 in c3 \ c6 ;
then E26: ( c8 in c3 & not c8 in c6 ) by XBOOLE_0:def 4;
per cases ( c9 in c3 \ c6 or c9 in {c5} ) by E25, XBOOLE_0:def 2;
suppose c9 in c3 \ c6 ;
then ( c9 in c3 & not c9 in c6 ) by XBOOLE_0:def 4;
hence c8 misses c9 by E25, E26, Def5;
end;
suppose c9 in {c5} ;
then c9 = c5 by TARSKI:def 1;
hence c8 misses c9 by E24, E25, E26;
end;
end;
end;
suppose c8 in {c5} ;
then E26: c8 = c5 by TARSKI:def 1;
per cases ( c9 in c3 \ c6 or c9 in {c5} ) by E25, XBOOLE_0:def 2;
suppose c9 in c3 \ c6 ;
then ( c9 in c3 & not c9 in c6 ) by XBOOLE_0:def 4;
hence c8 misses c9 by E24, E25, E26;
end;
suppose c9 in {c5} ;
hence c8 misses c9 by E25, E26, TARSKI:def 1;
end;
end;
end;
end;
end;
then E25: (c3 \ c6) \/ {c5} is mutually-disjoint Subset-Family of c1 by E23, Def5;
union c3 c= union ((c3 \ c6) \/ {c5})
proof
let c8 be set ; :: according to TARSKI:def 3
assume E26: c8 in union c3 ;
consider c9 being set such that
E27: ( c8 in c9 & c9 in c3 ) by E26, TARSKI:def 4;
per cases ( c9 in c6 or not c9 in c6 ) ;
suppose c9 in c6 ;
then c9 c= c5 by E18;
hence c8 in union ((c3 \ c6) \/ {c5}) by E19, E27, TARSKI:def 4;
end;
suppose not c9 in c6 ;
then c9 in c3 \ c6 by E27, XBOOLE_0:def 4;
hence c8 in union ((c3 \ c6) \/ {c5}) by E20, E27, TARSKI:def 4;
end;
end;
end;
then E26: c3 = (c3 \ c6) \/ {c5} by E14, E22, E25;
E27: {c5} c= (c3 \ c6) \/ {c5} by XBOOLE_1:7;
c5 in {c5} by TARSKI:def 1;
hence contradiction by E16, E17, E26, E27, TARSKI:def 4;
end;
hence c4 in union c3 ;
end;
end;
end;

E13: now
let c1 be set ;
let c2 be Hierarchy of c1;
let c3 be mutually-disjoint Subset-Family of c1;
assume E14: ( c3 c= c2 & ( for b1 being mutually-disjoint Subset-Family of c1 st b1 c= c2 & union c3 c= union b1 holds
c3 = b1 ) ) ;
let c4 be Subset of c1;
assume E15: c4 in c3 ;
now
assume E16: c4 = {} ;
set c5 = c3 \ {{} };
E17: union c3 c= union (c3 \ {{} })
proof
let c6 be set ; :: according to TARSKI:def 3
assume E18: c6 in union c3 ;
consider c7 being set such that
E19: ( c6 in c7 & c7 in c3 ) by E18, TARSKI:def 4;
not c7 in {{} } by E19, TARSKI:def 1;
then c7 in c3 \ {{} } by E19, XBOOLE_0:def 4;
hence c6 in union (c3 \ {{} }) by E19, TARSKI:def 4;
end;
E18: c3 \ {{} } c= c3 by XBOOLE_1:36;
then E19: c3 \ {{} } c= c2 by E14, XBOOLE_1:1;
c3 \ {{} } c= bool c1 by E18, XBOOLE_1:1;
then E20: c3 \ {{} } is Subset-Family of c1 ;
c3 \ {{} } is mutually-disjoint
proof
let c6, c7 be set ; :: according to TAXONOM2:def 5
assume E21: ( c6 in c3 \ {{} } & c7 in c3 \ {{} } & c6 <> c7 ) ;
( c6 in c3 & c7 in c3 ) by E21, XBOOLE_0:def 4;
hence c6 misses c7 by E21, Def5;
end;
then c3 = c3 \ {{} } by E14, E17, E19, E20;
then not {} in {{} } by E15, E16, XBOOLE_0:def 4;
hence contradiction by TARSKI:def 1;
end;
hence c4 <> {} ;
end;

definition
let c1 be set ;
let c2 be Subset-Family of c1;
attr a2 is T_3 means :Def6: :: TAXONOM2:def 6
for b1 being Subset of a1 st b1 in a2 holds
for b2 being Element of a1 st not b2 in b1 holds
ex b3 being Subset of a1 st
( b2 in b3 & b3 in a2 & b1 misses b3 );
end;

:: deftheorem Def6 defines T_3 TAXONOM2:def 6 :
for b1 being set
for b2 being Subset-Family of b1 holds
( b2 is T_3 iff for b3 being Subset of b1 st b3 in b2 holds
for b4 being Element of b1 st not b4 in b3 holds
ex b5 being Subset of b1 st
( b4 in b5 & b5 in b2 & b3 misses b5 ) );

theorem Th11: :: TAXONOM2:11
for b1 being set
for b2 being Subset-Family of b1 st b2 = {} holds
b2 is T_3
proof end;

registration
let c1 be set ;
cluster covering T_3 Hierarchy of a1;
existence
ex b1 being Hierarchy of c1 st
( b1 is covering & b1 is T_3 )
proof end;
end;

definition
let c1 be set ;
let c2 be Subset-Family of c1;
attr a2 is lower-bounded means :Def7: :: TAXONOM2:def 7
for b1 being set st b1 <> {} & b1 c= a2 & b1 is c=-linear holds
ex b2 being set st
( b2 in a2 & b2 c= meet b1 );
end;

:: deftheorem Def7 defines lower-bounded TAXONOM2:def 7 :
for b1 being set
for b2 being Subset-Family of b1 holds
( b2 is lower-bounded iff for b3 being set st b3 <> {} & b3 c= b2 & b3 is c=-linear holds
ex b4 being set st
( b4 in b2 & b4 c= meet b3 ) );

theorem Th12: :: TAXONOM2:12
for b1 being set
for b2 being Subset of b1
for b3 being mutually-disjoint Subset-Family of b1 st ( for b4 being set st b4 in b3 holds
( b2 misses b4 & b1 <> {} ) ) holds
( b3 \/ {b2} is mutually-disjoint Subset-Family of b1 & ( b2 <> {} implies union (b3 \/ {b2}) <> union b3 ) )
proof end;

definition
let c1 be set ;
let c2 be Subset-Family of c1;
attr a2 is with_max's means :Def8: :: TAXONOM2:def 8
for b1 being Subset of a1 st b1 in a2 holds
ex b2 being Subset of a1 st
( b1 c= b2 & b2 in a2 & ( for b3 being Subset of a1 st b2 c= b3 & b3 in a2 holds
b3 = a1 ) );
end;

:: deftheorem Def8 defines with_max's TAXONOM2:def 8 :
for b1 being set
for b2 being Subset-Family of b1 holds
( b2 is with_max's iff for b3 being Subset of b1 st b3 in b2 holds
ex b4 being Subset of b1 st
( b3 c= b4 & b4 in b2 & ( for b5 being Subset of b1 st b4 c= b5 & b5 in b2 holds
b5 = b1 ) ) );

theorem Th13: :: TAXONOM2:13
for b1 being set
for b2 being covering Hierarchy of b1 st b2 is with_max's holds
ex b3 being a_partition of b1 st b3 c= b2
proof end;

theorem Th14: :: TAXONOM2:14
for b1 being set
for b2 being covering Hierarchy of b1
for b3 being mutually-disjoint Subset-Family of b1 st b3 c= b2 & ( for b4 being mutually-disjoint Subset-Family of b1 st b4 c= b2 & union b3 c= union b4 holds
b3 = b4 ) holds
b3 is a_partition of b1
proof end;

theorem Th15: :: TAXONOM2:15
for b1 being set
for b2 being covering T_3 Hierarchy of b1 st b2 is lower-bounded & not {} in b2 holds
for b3 being Subset of b1
for b4 being mutually-disjoint Subset-Family of b1 st b3 in b4 & b4 c= b2 & ( for b5 being mutually-disjoint Subset-Family of b1 st b3 in b5 & b5 c= b2 & union b4 c= union b5 holds
union b4 = union b5 ) holds
b4 is a_partition of b1
proof end;

theorem Th16: :: TAXONOM2:16
for b1 being set
for b2 being covering T_3 Hierarchy of b1 st b2 is lower-bounded & not {} in b2 holds
for b3 being Subset of b1
for b4 being mutually-disjoint Subset-Family of b1 st b3 in b4 & b4 c= b2 & ( for b5 being mutually-disjoint Subset-Family of b1 st b3 in b5 & b5 c= b2 & b4 c= b5 holds
b4 = b5 ) holds
b4 is a_partition of b1
proof end;

theorem Th17: :: TAXONOM2:17
for b1 being set
for b2 being covering T_3 Hierarchy of b1 st b2 is lower-bounded & not {} in b2 holds
for b3 being Subset of b1 st b3 in b2 holds
ex b4 being a_partition of b1 st
( b3 in b4 & b4 c= b2 )
proof end;

E21: now
let c1 be non empty set ;
let c2 be set ;
assume E22: c1 c= c2 ;
consider c3 being set such that
E23: c3 in c1 by XBOOLE_0:def 1;
thus c1 meets c2 by E22, E23, XBOOLE_0:3;
end;

theorem Th18: :: TAXONOM2:18
for b1, b2 being non empty set
for b3 being a_partition of b1
for b4 being set st b4 in b3 & b2 c= b4 holds
for b5 being a_partition of b1 st b2 in b5 & ( for b6 being set holds
( not b6 in b5 or b6 c= b4 or b4 c= b6 or b4 misses b6 ) ) holds
for b6 being set st ( for b7 being set holds
( b7 in b6 iff ( b7 in b5 & b7 c= b4 ) ) ) holds
( b6 \/ (b3 \ {b4}) is a_partition of b1 & b6 \/ (b3 \ {b4}) is_finer_than b3 )
proof end;

theorem Th19: :: TAXONOM2:19
for b1, b2 being non empty set st b2 c= b1 holds
for b3 being a_partition of b1 st ex b4 being set st
( b4 in b3 & b4 c= b2 ) & ( for b4 being set holds
( not b4 in b3 or b4 c= b2 or b2 c= b4 or b2 misses b4 ) ) holds
for b4 being set st ( for b5 being set holds
( b5 in b4 iff ( b5 in b3 & b5 misses b2 ) ) ) holds
( b4 \/ {b2} is a_partition of b1 & b3 is_finer_than b4 \/ {b2} & ( for b5 being a_partition of b1 st b3 is_finer_than b5 holds
for b6 being set st b6 in b5 & b2 c= b6 holds
b4 \/ {b2} is_finer_than b5 ) )
proof end;

theorem Th20: :: TAXONOM2:20
for b1 being non empty set
for b2 being covering T_3 Hierarchy of b1 st b2 is lower-bounded & not {} in b2 & ( for b3 being set st b3 <> {} & b3 c= PARTITIONS b1 & ( for b4, b5 being set st b4 in b3 & b5 in b3 & not b4 is_finer_than b5 holds
b5 is_finer_than b4 ) holds
ex b4, b5 being set st
( b4 in b3 & b5 in b3 & ( for b6 being set st b6 in b3 holds
( b6 is_finer_than b5 & b4 is_finer_than b6 ) ) ) ) holds
ex b3 being Classification of b1 st union b3 = b2
proof end;