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 B' = union C as non empty set by A2, TARSKI:def 4;
set R' = RelIncl (union C);
reconsider R = RelIncl (union C) as Relation of ;
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

let x, y be Element of ; :: thesis: ( for z being Element of holds
( not z <= x or not z <= y ) or x <= y or y <= x )
given z being Element of such that A8: z <= x and
A9: z <= y ; :: thesis: ( x <= y or y <= x )
reconsider z' = z as Element of B' ;
reconsider z'' = z' as Subset of by A4, Th4;
consider Z being set such that
A10: z' in Z and
A11: Z in C by TARSKI:def 4;
reconsider Z' = Z as a_partition of X by A3, A11, PARTIT1:def 3;
z'' in Z' by A10;
then z'' <> {} by EQREL_1:def 6;
then consider a being set such that
A12: a in z by XBOOLE_0:def 1;
[z,y] in R by A9, ORDERS_2:def 9;
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 x' = x, y' = y as Element of B' ;
consider S being set such that
A16: x' in S and
A17: S in C by TARSKI:def 4;
reconsider S' = S as a_partition of X by A3, A17, PARTIT1:def 3;
consider T being set such that
A18: y' in T and
A19: T in C by TARSKI:def 4;
reconsider T' = T as a_partition of X by A3, A19, PARTIT1:def 3;
[z,x] in R by A8, ORDERS_2:def 9;
then A20: z c= x by A6, WELLORD2:def 1;
then A21: a in x by A12;

now

per cases ( S' is_finer_than T' or T' is_finer_than S' ) by A17, A19, A15, TAXONOM1:def 1;

suppose S' is_finer_than T' ; :: thesis: ( x' c= y' or y' c= x' )

then ex Y being set st
( Y in T' & x' c= Y ) by A16, SETFAM_1:def 2;
hence ( x' c= y' or y' c= x' ) by A12, A21, A13, A18, Th3; :: thesis: verum

end;

suppose T' is_finer_than S' ; :: thesis: ( x' c= y' or y' c= x' )

then ex Y being set st
( Y in S' & y' c= Y ) by A18, SETFAM_1:def 2;
hence ( x' c= y' or y' c= x' ) by A12, A20, A14, A16, Th3; :: thesis: verum

end;

end;

end;

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;

A22: RelStr(# (union C),R #) is with_superior

proof

reconsider C' = C as Strong_Classification of X by A3;
reconsider s = X as Element of by A5, A2, TARSKI:def 4;
consider x being set such that
A23: x in SmallestPartition X by XBOOLE_0:def 1;
SmallestPartition X in C' by TAXONOM1:def 2;
then reconsider x' = x as Element of 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

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 y' = y as Element of B' ;
y' c= s by A4, Th4;
hence [y,s] in R by WELLORD2:def 1; :: thesis: verum

end;

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

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

end;

end;

end;

[x',s] in R by A6, A23, WELLORD2:def 1;
then s in field R by RELAT_1:30;
hence s is_superior_of the InternalRel of RelStr(# (union C),R #) by A24, ORDERS_1:def 13; :: 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