let X be non empty set ; :: thesis: 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 ; :: thesis: ( C is Strong_Classification of X implies InclPoset (union C) is Tree )
assume A3: C is Strong_Classification of X ; :: thesis: 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 :: thesis: 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 #); :: 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 A8: z <= x and
A9: z <= y ; :: thesis: ( 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;

now :: thesis: ( x9 c= y9 or y9 c= x9 )

per cases ( S9 is_finer_than T9 or T9 is_finer_than S9 ) by A17, A19, A15, TAXONOM1:def 1;

suppose S9 is_finer_than T9 ; :: thesis: ( x9 c= y9 or y9 c= x9 )

then ex Y being set st
( Y in T9 & x9 c= Y ) by A16;
hence ( x9 c= y9 or y9 c= x9 ) by A12, A21, A13, A18, Lm1; :: thesis: verum

end;

suppose T9 is_finer_than S9 ; :: thesis: ( x9 c= y9 or y9 c= x9 )

then ex Y being set st
( Y in S9 & y9 c= Y ) by A18;
hence ( x9 c= y9 or y9 c= x9 ) by A12, A20, A14, A16, Lm1; :: thesis: verum

end;

end;

end;

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; :: thesis: 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 ; :: according to TAXONOM2:def 1 :: thesis: s is_superior_of the InternalRel of RelStr(# (union C),R #)

A24: now :: thesis: for y being set st y in field R & y <> s holds
[y,s] in R

let y be set ; :: thesis: ( y in field R & y <> s implies [b₁,s] in R )
assume that
A25: y in field R and
y <> s ; :: thesis: [b₁,s] in R
A26: y in (dom R) \/ (rng R) by A25, RELAT_1:def 6;

per cases ( y in dom R or y in rng R ) by A26, XBOOLE_0:def 3;

suppose y in dom R ; :: thesis: [b₁,s] in R

then reconsider y9 = y as Element of B9 ;
y9 c= s by A4, Th3;
hence [y,s] in R by WELLORD2:def 1; :: thesis: verum

end;

suppose y in rng R ; :: thesis: [b₁,s] in R

then reconsider y9 = y as Element of B9 ;
y9 c= s by A4, Th3;
hence [y,s] in R by WELLORD2:def 1; :: thesis: verum

end;

end;

end;

[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; :: thesis: verum

end;

RelStr(# (union C),R #) = InclPoset (union C) by YELLOW_1:def 1;
hence InclPoset (union C) is Tree by A22, A7, Def2; :: thesis: verum