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;

hence InclPoset (union C) is Tree by A22, A7, Def2; :: thesis: verum

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 )

A22:
RelStr(# (union C),R #) is with_superior
( 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;

hence ( x <= y or y <= x ) by ORDERS_2:def 5; :: thesis: verum

end;( 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 )end;

then
( [x9,y9] in R or [y9,x9] in R )
by WELLORD2:def 1;per cases
( S9 is_finer_than T9 or T9 is_finer_than S9 )
by A17, A19, A15, TAXONOM1:def 1;

end;

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;( Y in T9 & x9 c= Y ) by A16;

hence ( x9 c= y9 or y9 c= x9 ) by A12, A21, A13, A18, Lm1; :: thesis: verum

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;( Y in S9 & y9 c= Y ) by A18;

hence ( x9 c= y9 or y9 c= x9 ) by A12, A20, A14, A16, Lm1; :: thesis: verum

hence ( x <= y or y <= x ) by ORDERS_2:def 5; :: thesis: verum

proof

RelStr(# (union C),R #) = InclPoset (union C)
by YELLOW_1:def 1;
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 #)

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;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

[x9,s] in R
by A6, A23, WELLORD2:def 1;[y,s] in R

let y be set ; :: thesis: ( y in field R & y <> s implies [b_{1},s] in R )

assume that

A25: y in field R and

y <> s ; :: thesis: [b_{1},s] in R

A26: y in (dom R) \/ (rng R) by A25, RELAT_1:def 6;

end;assume that

A25: y in field R and

y <> s ; :: thesis: [b

A26: y in (dom R) \/ (rng R) by A25, RELAT_1:def 6;

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

hence InclPoset (union C) is Tree by A22, A7, Def2; :: thesis: verum