let X be non empty set ; :: thesis: for C being set st C is Strong_Classification of X holds
InclPoset (union C) is Tree
let C be set ; :: thesis: ( C is Strong_Classification of X implies InclPoset (union C) is Tree )
assume A1:
C is Strong_Classification of X
; :: thesis: InclPoset (union C) is Tree
set B = union C;
A2:
X in {X}
by TARSKI:def 1;
{X} in C
by A1, TAXONOM1:def 2;
then A3:
union C <> {}
by A2, TARSKI:def 4;
set R' = RelIncl (union C);
reconsider R = RelIncl (union C) as Relation of (union C) ;
A4:
RelStr(# (union C),R #) = InclPoset (union C)
by YELLOW_1:def 1;
set D = RelStr(# (union C),R #);
A5:
C is Classification of X
by A1, TAXONOM1:def 2;
A6:
{X} in C
by A1, TAXONOM1:def 2;
A7:
X in {X}
by TARSKI:def 1;
then reconsider B' = union C as non empty set by A6, TARSKI:def 4;
A8:
RelStr(# (union C),R #) is with_superior
proof
reconsider s =
X as
Element of
RelStr(#
(union C),
R #)
by A6, A7, TARSKI:def 4;
consider x being
set such that A9:
x in SmallestPartition X
by XBOOLE_0:def 1;
reconsider C' =
C as
Strong_Classification of
X by A1;
SmallestPartition X in C'
by TAXONOM1:def 2;
then reconsider x' =
x as
Element of
RelStr(#
(union C),
R #)
by A9, TARSKI:def 4;
take
s
;
:: according to TAXONOM2:def 1 :: thesis: s is_superior_of the InternalRel of RelStr(# (union C),R #)
[x',s] in R
by A3, A9, WELLORD2:def 1;
then A10:
s in field R
by RELAT_1:30;
hence
s is_superior_of the
InternalRel of
RelStr(#
(union C),
R #)
by A10, ORDERS_1:def 13;
:: thesis: verum
end;
now let x,
y be
Element of
RelStr(#
(union C),
R #);
:: thesis: ( for z being Element of RelStr(# (union C),R #) holds
( not z <= x or not z <= y ) or x <= y or y <= x )given z being
Element of
RelStr(#
(union C),
R #)
such that A13:
(
z <= x &
z <= y )
;
:: thesis: ( x <= y or y <= x )reconsider z' =
z as
Element of
B' ;
consider Z being
set such that A14:
(
z' in Z &
Z in C )
by TARSKI:def 4;
reconsider z'' =
z' as
Subset of
X by A5, Th4;
reconsider Z' =
Z as
a_partition of
X by A1, A14, PARTIT1:def 3;
z'' in Z'
by A14;
then
z'' <> {}
by EQREL_1:def 6;
then consider a being
set such that A15:
a in z
by XBOOLE_0:def 1;
[z,x] in R
by A13, ORDERS_2:def 9;
then A16:
z c= x
by A3, WELLORD2:def 1;
then A17:
a in x
by A15;
[z,y] in R
by A13, ORDERS_2:def 9;
then A18:
z c= y
by A3, WELLORD2:def 1;
then A19:
a in y
by A15;
reconsider x' =
x,
y' =
y as
Element of
B' ;
consider S being
set such that A20:
(
x' in S &
S in C )
by TARSKI:def 4;
reconsider S' =
S as
a_partition of
X by A1, A20, PARTIT1:def 3;
consider T being
set such that A21:
(
y' in T &
T in C )
by TARSKI:def 4;
reconsider T' =
T as
a_partition of
X by A1, A21, PARTIT1:def 3;
A22:
C is
Classification of
X
by A1, TAXONOM1:def 2;
then
(
[x',y'] in R or
[y',x'] in R )
by WELLORD2:def 1;
hence
(
x <= y or
y <= x )
by ORDERS_2:def 9;
:: thesis: verum end;
hence
InclPoset (union C) is Tree
by A4, A8, Def2; :: thesis: verum