let X be non empty set ; for C being set st C is Strong_Classification of X holds
InclPoset (union C) is Tree
A1:
X in {X}
by TARSKI:def 1;
A2:
X in {X}
by TARSKI:def 1;
let C be set ; ( C is Strong_Classification of X implies InclPoset (union C) is Tree )
assume A3:
C is Strong_Classification of X
; InclPoset (union C) is Tree
A4:
C is Classification of X
by A3, TAXONOM1:def 2;
set B = union C;
A5:
{X} in C
by A3, TAXONOM1:def 2;
then reconsider B9 = union C as non empty set by A2, TARSKI:def 4;
set R9 = RelIncl (union C);
reconsider R = RelIncl (union C) as Relation of (union C) ;
set D = RelStr(# (union C),R #);
{X} in C
by A3, TAXONOM1:def 2;
then A6:
union C <> {}
by A1, TARSKI:def 4;
A7:
now for x, y being Element of RelStr(# (union C),R #) holds
( for z being Element of RelStr(# (union C),R #) holds
( not z <= x or not z <= y ) or x <= y or y <= x )let x,
y be
Element of
RelStr(#
(union C),
R #);
( 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 A8:
z <= x
and A9:
z <= y
;
( x <= y or y <= x )reconsider z9 =
z as
Element of
B9 ;
reconsider z99 =
z9 as
Subset of
X by A4, Th3;
consider Z being
set such that A10:
z9 in Z
and A11:
Z in C
by TARSKI:def 4;
reconsider Z9 =
Z as
a_partition of
X by A3, A11, PARTIT1:def 3;
z99 in Z9
by A10;
then
z99 <> {}
by EQREL_1:def 4;
then consider a being
object such that A12:
a in z
by XBOOLE_0:def 1;
[z,y] in R
by A9, ORDERS_2:def 5;
then A13:
z c= y
by A6, WELLORD2:def 1;
then A14:
a in y
by A12;
A15:
C is
Classification of
X
by A3, TAXONOM1:def 2;
reconsider x9 =
x,
y9 =
y as
Element of
B9 ;
consider S being
set such that A16:
x9 in S
and A17:
S in C
by TARSKI:def 4;
reconsider S9 =
S as
a_partition of
X by A3, A17, PARTIT1:def 3;
consider T being
set such that A18:
y9 in T
and A19:
T in C
by TARSKI:def 4;
reconsider T9 =
T as
a_partition of
X by A3, A19, PARTIT1:def 3;
[z,x] in R
by A8, ORDERS_2:def 5;
then A20:
z c= x
by A6, WELLORD2:def 1;
then A21:
a in x
by A12;
then
(
[x9,y9] in R or
[y9,x9] in R )
by WELLORD2:def 1;
hence
(
x <= y or
y <= x )
by ORDERS_2:def 5;
verum end;
A22:
RelStr(# (union C),R #) is with_superior
proof
reconsider C9 =
C as
Strong_Classification of
X by A3;
reconsider s =
X as
Element of
RelStr(#
(union C),
R #)
by A5, A2, TARSKI:def 4;
consider x being
object such that A23:
x in SmallestPartition X
by XBOOLE_0:def 1;
SmallestPartition X in C9
by TAXONOM1:def 2;
then reconsider x9 =
x as
Element of
RelStr(#
(union C),
R #)
by A23, TARSKI:def 4;
take
s
;
TAXONOM2:def 1 s is_superior_of the InternalRel of RelStr(# (union C),R #)
[x9,s] in R
by A6, A23, WELLORD2:def 1;
then
s in field R
by RELAT_1:15;
hence
s is_superior_of the
InternalRel of
RelStr(#
(union C),
R #)
by A24, ORDERS_1:def 14;
verum
end;
RelStr(# (union C),R #) = InclPoset (union C)
by YELLOW_1:def 1;
hence
InclPoset (union C) is Tree
by A22, A7, Def2; verum