:: TAXONOM2 semantic presentation
begin
definition
let A be RelStr ;
attrA is with_superior means :: TAXONOM2:def 1
ex x being Element of A st x is_superior_of the InternalRel of A;
end;
:: deftheorem defines with_superior TAXONOM2:def_1_:_
for A being RelStr holds
( A is with_superior iff ex x being Element of A st x is_superior_of the InternalRel of A );
definition
let A be RelStr ;
attrA is with_comparable_down means :Def2: :: TAXONOM2:def 2
for x, y being Element of A holds
( for z being Element of A holds
( not z <= x or not z <= y ) or x <= y or y <= x );
end;
:: deftheorem Def2 defines with_comparable_down TAXONOM2:def_2_:_
for A being RelStr holds
( A is with_comparable_down iff for x, y being Element of A holds
( for z being Element of A holds
( not z <= x or not z <= y ) or x <= y or y <= x ) );
theorem Th1: :: TAXONOM2:1
for a being set holds
( not InclPoset {{a}} is empty & InclPoset {{a}} is reflexive & InclPoset {{a}} is transitive & InclPoset {{a}} is antisymmetric & InclPoset {{a}} is with_superior & InclPoset {{a}} is with_comparable_down )
proof
let a be set ; ::_thesis: ( not InclPoset {{a}} is empty & InclPoset {{a}} is reflexive & InclPoset {{a}} is transitive & InclPoset {{a}} is antisymmetric & InclPoset {{a}} is with_superior & InclPoset {{a}} is with_comparable_down )
set A = {{a}};
set R9 = RelIncl {{a}};
reconsider R = RelIncl {{a}} as Relation of {{a}} ;
set L = RelStr(# {{a}},R #);
A1: RelStr(# {{a}},R #) is with_superior
proof
set max1 = {a};
reconsider max9 = {a} as Element of RelStr(# {{a}},R #) by TARSKI:def_1;
take max9 ; :: according to TAXONOM2:def_1 ::_thesis: max9 is_superior_of the InternalRel of RelStr(# {{a}},R #)
A2: for y being set st y in field R & y <> max9 holds
[y,max9] in R
proof
let y be set ; ::_thesis: ( y in field R & y <> max9 implies [y,max9] in R )
assume that
A3: y in field R and
A4: y <> max9 ; ::_thesis: [y,max9] in R
field R c= {{a}} \/ {{a}} by RELSET_1:8;
hence [y,max9] in R by A3, A4, TARSKI:def_1; ::_thesis: verum
end;
[max9,max9] in R by WELLORD2:def_1;
then max9 in field R by RELAT_1:15;
hence max9 is_superior_of the InternalRel of RelStr(# {{a}},R #) by A2, ORDERS_1:def_13; ::_thesis: verum
end;
A5: for x, y being Element of RelStr(# {{a}},R #) holds
( for z being Element of RelStr(# {{a}},R #) holds
( not z <= x or not z <= y ) or x <= y or y <= x )
proof
let x, y be Element of RelStr(# {{a}},R #); ::_thesis: ( for z being Element of RelStr(# {{a}},R #) holds
( not z <= x or not z <= y ) or x <= y or y <= x )
assume ex z being Element of RelStr(# {{a}},R #) st
( z <= x & z <= y ) ; ::_thesis: ( x <= y or y <= x )
A6: y = {a} by TARSKI:def_1;
x = {a} by TARSKI:def_1;
then [x,y] in R by A6, WELLORD2:def_1;
hence ( x <= y or y <= x ) by ORDERS_2:def_5; ::_thesis: verum
end;
RelStr(# {{a}},R #) = InclPoset {{a}} by YELLOW_1:def_1;
hence ( not InclPoset {{a}} is empty & InclPoset {{a}} is reflexive & InclPoset {{a}} is transitive & InclPoset {{a}} is antisymmetric & InclPoset {{a}} is with_superior & InclPoset {{a}} is with_comparable_down ) by A1, A5, Def2; ::_thesis: verum
end;
registration
cluster non empty strict reflexive transitive antisymmetric with_superior with_comparable_down for RelStr ;
existence
ex b1 being RelStr st
( not b1 is empty & b1 is reflexive & b1 is transitive & b1 is antisymmetric & b1 is with_superior & b1 is with_comparable_down & b1 is strict )
proof
take InclPoset {{{}}} ; ::_thesis: ( not InclPoset {{{}}} is empty & InclPoset {{{}}} is reflexive & InclPoset {{{}}} is transitive & InclPoset {{{}}} is antisymmetric & InclPoset {{{}}} is with_superior & InclPoset {{{}}} is with_comparable_down & InclPoset {{{}}} is strict )
thus ( not InclPoset {{{}}} is empty & InclPoset {{{}}} is reflexive & InclPoset {{{}}} is transitive & InclPoset {{{}}} is antisymmetric & InclPoset {{{}}} is with_superior & InclPoset {{{}}} is with_comparable_down & InclPoset {{{}}} is strict ) by Th1; ::_thesis: verum
end;
end;
definition
mode Tree is with_superior with_comparable_down Poset;
end;
theorem Th2: :: TAXONOM2:2
for X being non empty set
for EqR being Equivalence_Relation of X
for x, y, z being set st z in Class (EqR,x) & z in Class (EqR,y) holds
Class (EqR,x) = Class (EqR,y)
proof
let X be non empty set ; ::_thesis: for EqR being Equivalence_Relation of X
for x, y, z being set st z in Class (EqR,x) & z in Class (EqR,y) holds
Class (EqR,x) = Class (EqR,y)
let EqR be Equivalence_Relation of X; ::_thesis: for x, y, z being set st z in Class (EqR,x) & z in Class (EqR,y) holds
Class (EqR,x) = Class (EqR,y)
let x, y, z be set ; ::_thesis: ( z in Class (EqR,x) & z in Class (EqR,y) implies Class (EqR,x) = Class (EqR,y) )
assume that
A1: z in Class (EqR,x) and
A2: z in Class (EqR,y) ; ::_thesis: Class (EqR,x) = Class (EqR,y)
A3: [z,y] in EqR by A2, EQREL_1:19;
[z,x] in EqR by A1, EQREL_1:19;
hence Class (EqR,x) = Class (EqR,z) by A1, EQREL_1:35
.= Class (EqR,y) by A1, A3, EQREL_1:35 ;
::_thesis: verum
end;
theorem :: TAXONOM2:3
canceled;
Th3: for X being non empty set
for P being a_partition of X
for x, y, z being set st x in P & y in P & z in x & z in y holds
x = y
by EQREL_1:70;
theorem Th4: :: TAXONOM2:4
for X being non empty set
for C, x being set st C is Classification of X & x in union C holds
x c= X
proof
let X be non empty set ; ::_thesis: for C, x being set st C is Classification of X & x in union C holds
x c= X
let C, x be set ; ::_thesis: ( C is Classification of X & x in union C implies x c= X )
assume that
A1: C is Classification of X and
A2: x in union C ; ::_thesis: x c= X
consider Y being set such that
A3: x in Y and
A4: Y in C by A2, TARSKI:def_4;
reconsider Y9 = Y as a_partition of X by A1, A4, PARTIT1:def_3;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in x or a in X )
assume a in x ; ::_thesis: a in X
then a in union Y9 by A3, TARSKI:def_4;
hence a in X ; ::_thesis: verum
end;
theorem :: TAXONOM2:5
for X being non empty set
for C being set st C is Strong_Classification of X holds
InclPoset (union C) is Tree
proof
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, Th4;
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 set 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_)
percases ( 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, SETFAM_1:def_2;
hence ( x9 c= y9 or y9 c= x9 ) by A12, A21, A13, A18, Th3; ::_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, SETFAM_1:def_2;
hence ( x9 c= y9 or y9 c= x9 ) by A12, A20, A14, A16, Th3; ::_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 set 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 [b1,s] in R )
assume that
A25: y in field R and
y <> s ; ::_thesis: [b1,s] in R
A26: y in (dom R) \/ (rng R) by A25, RELAT_1:def_6;
percases ( y in dom R or y in rng R ) by A26, XBOOLE_0:def_3;
suppose y in dom R ; ::_thesis: [b1,s] in R
then reconsider y9 = y as Element of B9 ;
y9 c= s by A4, Th4;
hence [y,s] in R by WELLORD2:def_1; ::_thesis: verum
end;
suppose y in rng R ; ::_thesis: [b1,s] in R
then reconsider y9 = y as Element of B9 ;
y9 c= s by A4, Th4;
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_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
end;
begin
definition
let Y be set ;
attrY is hierarchic means :Def3: :: TAXONOM2:def 3
for x, y being set st x in Y & y in Y & not x c= y & not y c= x holds
x misses y;
end;
:: deftheorem Def3 defines hierarchic TAXONOM2:def_3_:_
for Y being set holds
( Y is hierarchic iff for x, y being set st x in Y & y in Y & not x c= y & not y c= x holds
x misses y );
registration
cluster trivial -> hierarchic for set ;
coherence
for b1 being set st b1 is trivial holds
b1 is hierarchic
proof
let X be set ; ::_thesis: ( X is trivial implies X is hierarchic )
assume A1: X is trivial ; ::_thesis: X is hierarchic
percases ( X is empty or ex a being set st X = {a} ) by A1, ZFMISC_1:131;
supposeA2: X is empty ; ::_thesis: X is hierarchic
for x, y being set st x in {} & y in {} & not x c= y & not y c= x holds
x misses y ;
hence X is hierarchic by A2, Def3; ::_thesis: verum
end;
suppose ex a being set st X = {a} ; ::_thesis: X is hierarchic
then consider a being set such that
A3: X = {a} ;
X is hierarchic
proof
let x, y be set ; :: according to TAXONOM2:def_3 ::_thesis: ( x in X & y in X & not x c= y & not y c= x implies x misses y )
assume that
A4: x in X and
A5: y in X ; ::_thesis: ( x c= y or y c= x or x misses y )
x = a by A3, A4, TARSKI:def_1;
hence ( x c= y or y c= x or x misses y ) by A3, A5, TARSKI:def_1; ::_thesis: verum
end;
hence X is hierarchic ; ::_thesis: verum
end;
end;
end;
end;
registration
cluster non trivial hierarchic for set ;
existence
ex b1 being set st
( not b1 is trivial & b1 is hierarchic )
proof
set B = the empty set ;
set A = the non empty set ;
consider C being set such that
A1: C = { the non empty set , the empty set } ;
A2: C is hierarchic
proof
let x, y be set ; :: according to TAXONOM2:def_3 ::_thesis: ( x in C & y in C & not x c= y & not y c= x implies x misses y )
assume that
A3: x in C and
A4: y in C ; ::_thesis: ( x c= y or y c= x or x misses y )
percases ( x = the non empty set or x = the empty set ) by A1, A3, TARSKI:def_2;
supposeA5: x = the non empty set ; ::_thesis: ( x c= y or y c= x or x misses y )
percases ( y = the non empty set or y = the empty set ) by A1, A4, TARSKI:def_2;
suppose y = the non empty set ; ::_thesis: ( x c= y or y c= x or x misses y )
hence ( x c= y or y c= x or x misses y ) by A5; ::_thesis: verum
end;
suppose y = the empty set ; ::_thesis: ( x c= y or y c= x or x misses y )
hence ( x c= y or y c= x or x misses y ) by XBOOLE_1:65; ::_thesis: verum
end;
end;
end;
suppose x = the empty set ; ::_thesis: ( x c= y or y c= x or x misses y )
hence ( x c= y or y c= x or x misses y ) by XBOOLE_1:65; ::_thesis: verum
end;
end;
end;
take C ; ::_thesis: ( not C is trivial & C is hierarchic )
now__::_thesis:_not_C_is_trivial
assume A6: C is trivial ; ::_thesis: contradiction
percases ( C is empty or ex x being set st C = {x} ) by A6, ZFMISC_1:131;
suppose C is empty ; ::_thesis: contradiction
hence contradiction by A1; ::_thesis: verum
end;
suppose ex x being set st C = {x} ; ::_thesis: contradiction
hence contradiction by A1, ZFMISC_1:5; ::_thesis: verum
end;
end;
end;
hence ( not C is trivial & C is hierarchic ) by A2; ::_thesis: verum
end;
end;
theorem Th6: :: TAXONOM2:6
{} is hierarchic
proof
let x, y be set ; :: according to TAXONOM2:def_3 ::_thesis: ( x in {} & y in {} & not x c= y & not y c= x implies x misses y )
assume that
A1: x in {} and
y in {} ; ::_thesis: ( x c= y or y c= x or x misses y )
thus ( x c= y or y c= x or x misses y ) by A1; ::_thesis: verum
end;
theorem :: TAXONOM2:7
{{}} is hierarchic
proof
let x, y be set ; :: according to TAXONOM2:def_3 ::_thesis: ( x in {{}} & y in {{}} & not x c= y & not y c= x implies x misses y )
assume that
A1: x in {{}} and
A2: y in {{}} ; ::_thesis: ( x c= y or y c= x or x misses y )
x = {} by A1, TARSKI:def_1;
hence ( x c= y or y c= x or x misses y ) by A2, TARSKI:def_1; ::_thesis: verum
end;
definition
let Y be set ;
mode Hierarchy of Y -> Subset-Family of Y means :Def4: :: TAXONOM2:def 4
it is hierarchic ;
existence
ex b1 being Subset-Family of Y st b1 is hierarchic
proof
set H = {} ;
reconsider H9 = {} as Subset-Family of Y by XBOOLE_1:2;
take H9 ; ::_thesis: H9 is hierarchic
thus H9 is hierarchic by Th6; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines Hierarchy TAXONOM2:def_4_:_
for Y being set
for b2 being Subset-Family of Y holds
( b2 is Hierarchy of Y iff b2 is hierarchic );
definition
let Y be set ;
attrY is mutually-disjoint means :Def5: :: TAXONOM2:def 5
for x, y being set st x in Y & y in Y & x <> y holds
x misses y;
end;
:: deftheorem Def5 defines mutually-disjoint TAXONOM2:def_5_:_
for Y being set holds
( Y is mutually-disjoint iff for x, y being set st x in Y & y in Y & x <> y holds
x misses y );
Lm1: now__::_thesis:_for_x,_y_being_set_st_x_in_{{}}_&_y_in_{{}}_&_x_<>_y_holds_
x_misses_y
let x, y be set ; ::_thesis: ( x in {{}} & y in {{}} & x <> y implies x misses y )
assume that
A1: x in {{}} and
A2: y in {{}} and
A3: x <> y ; ::_thesis: x misses y
x = {} by A1, TARSKI:def_1;
hence x misses y by A2, A3, TARSKI:def_1; ::_thesis: verum
end;
registration
let Y be set ;
cluster mutually-disjoint for Element of bool (bool Y);
existence
ex b1 being Subset-Family of Y st b1 is mutually-disjoint
proof
set e = {{}};
now__::_thesis:_for_x_being_set_st_x_in_{{}}_holds_
x_in_bool_Y
let x be set ; ::_thesis: ( x in {{}} implies x in bool Y )
assume x in {{}} ; ::_thesis: x in bool Y
then x = {} by TARSKI:def_1;
then x c= Y by XBOOLE_1:2;
hence x in bool Y ; ::_thesis: verum
end;
then reconsider e9 = {{}} as Subset-Family of Y by TARSKI:def_3;
take e9 ; ::_thesis: e9 is mutually-disjoint
thus e9 is mutually-disjoint by Def5, Lm1; ::_thesis: verum
end;
end;
theorem :: TAXONOM2:8
{} is mutually-disjoint
proof
let x, y be set ; :: according to TAXONOM2:def_5 ::_thesis: ( x in {} & y in {} & x <> y implies x misses y )
assume that
A1: x in {} and
y in {} ; ::_thesis: ( not x <> y or x misses y )
thus ( not x <> y or x misses y ) by A1; ::_thesis: verum
end;
theorem :: TAXONOM2:9
{{}} is mutually-disjoint by Def5, Lm1;
theorem Th10: :: TAXONOM2:10
for a being set holds {a} is mutually-disjoint
proof
let a be set ; ::_thesis: {a} is mutually-disjoint
let x, y be set ; :: according to TAXONOM2:def_5 ::_thesis: ( x in {a} & y in {a} & x <> y implies x misses y )
assume that
A1: x in {a} and
A2: y in {a} and
A3: x <> y ; ::_thesis: x misses y
x = a by A1, TARSKI:def_1;
hence x misses y by A2, A3, TARSKI:def_1; ::_thesis: verum
end;
Lm2: now__::_thesis:_for_Y_being_set_
for_H_being_Hierarchy_of_Y_st_H_is_covering_holds_
for_B_being_mutually-disjoint_Subset-Family_of_Y_st_B_c=_H_&_(_for_C_being_mutually-disjoint_Subset-Family_of_Y_st_C_c=_H_&_union_B_c=_union_C_holds_
B_=_C_)_holds_
union_B_=_Y
let Y be set ; ::_thesis: for H being Hierarchy of Y st H is covering holds
for B being mutually-disjoint Subset-Family of Y st B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds
B = C ) holds
union B = Y
let H be Hierarchy of Y; ::_thesis: ( H is covering implies for B being mutually-disjoint Subset-Family of Y st B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds
B = C ) holds
union B = Y )
assume A1: H is covering ; ::_thesis: for B being mutually-disjoint Subset-Family of Y st B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds
B = C ) holds
union B = Y
let B be mutually-disjoint Subset-Family of Y; ::_thesis: ( B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds
B = C ) implies union B = Y )
assume that
A2: B c= H and
A3: for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds
B = C ; ::_thesis: union B = Y
Y c= union B
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Y or y in union B )
assume y in Y ; ::_thesis: y in union B
then y in union H by A1, ABIAN:4;
then consider x being set such that
A4: y in x and
A5: x in H by TARSKI:def_4;
now__::_thesis:_y_in_union_B
defpred S1[ set ] means $1 c= x;
consider D being set such that
A6: for a being set holds
( a in D iff ( a in B & S1[a] ) ) from XBOOLE_0:sch_1();
set C = (B \ D) \/ {x};
A7: B \ D c= (B \ D) \/ {x} by XBOOLE_1:7;
A8: {x} c= H
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in {x} or s in H )
assume s in {x} ; ::_thesis: s in H
hence s in H by A5, TARSKI:def_1; ::_thesis: verum
end;
assume A9: not y in union B ; ::_thesis: contradiction
A10: for p being set st p in B & not p in D & p <> x holds
p misses x
proof
A11: H is hierarchic by Def4;
let p be set ; ::_thesis: ( p in B & not p in D & p <> x implies p misses x )
assume that
A12: p in B and
A13: not p in D and
p <> x ; ::_thesis: p misses x
A14: not x c= p by A4, A9, A12, TARSKI:def_4;
not p c= x by A6, A12, A13;
hence p misses x by A2, A5, A12, A14, A11, Def3; ::_thesis: verum
end;
A15: for p, q being set st p in (B \ D) \/ {x} & q in (B \ D) \/ {x} & p <> q holds
p misses q
proof
let p, q be set ; ::_thesis: ( p in (B \ D) \/ {x} & q in (B \ D) \/ {x} & p <> q implies p misses q )
assume that
A16: p in (B \ D) \/ {x} and
A17: q in (B \ D) \/ {x} and
A18: p <> q ; ::_thesis: p misses q
percases ( p in B \ D or p in {x} ) by A16, XBOOLE_0:def_3;
supposeA19: p in B \ D ; ::_thesis: p misses q
then A20: not p in D by XBOOLE_0:def_5;
A21: p in B by A19, XBOOLE_0:def_5;
percases ( q in B \ D or q in {x} ) by A17, XBOOLE_0:def_3;
suppose q in B \ D ; ::_thesis: p misses q
then q in B by XBOOLE_0:def_5;
hence p misses q by A18, A21, Def5; ::_thesis: verum
end;
suppose q in {x} ; ::_thesis: p misses q
then q = x by TARSKI:def_1;
hence p misses q by A10, A18, A21, A20; ::_thesis: verum
end;
end;
end;
suppose p in {x} ; ::_thesis: p misses q
then A22: p = x by TARSKI:def_1;
percases ( q in B \ D or q in {x} ) by A17, XBOOLE_0:def_3;
supposeA23: q in B \ D ; ::_thesis: p misses q
then A24: not q in D by XBOOLE_0:def_5;
q in B by A23, XBOOLE_0:def_5;
hence p misses q by A10, A18, A22, A24; ::_thesis: verum
end;
suppose q in {x} ; ::_thesis: p misses q
hence p misses q by A18, A22, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
end;
end;
x in {x} by TARSKI:def_1;
then A25: x in (B \ D) \/ {x} by XBOOLE_0:def_3;
A26: union B c= union ((B \ D) \/ {x})
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in union B or s in union ((B \ D) \/ {x}) )
assume s in union B ; ::_thesis: s in union ((B \ D) \/ {x})
then consider t being set such that
A27: s in t and
A28: t in B by TARSKI:def_4;
percases ( t in D or not t in D ) ;
suppose t in D ; ::_thesis: s in union ((B \ D) \/ {x})
then t c= x by A6;
hence s in union ((B \ D) \/ {x}) by A25, A27, TARSKI:def_4; ::_thesis: verum
end;
suppose not t in D ; ::_thesis: s in union ((B \ D) \/ {x})
then t in B \ D by A28, XBOOLE_0:def_5;
hence s in union ((B \ D) \/ {x}) by A7, A27, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
A29: x in {x} by TARSKI:def_1;
B \ D c= B by XBOOLE_1:36;
then A30: B \ D c= H by A2, XBOOLE_1:1;
then (B \ D) \/ {x} c= H by A8, XBOOLE_1:8;
then (B \ D) \/ {x} is mutually-disjoint Subset-Family of Y by A15, Def5, XBOOLE_1:1;
then A31: B = (B \ D) \/ {x} by A3, A30, A8, A26, XBOOLE_1:8;
{x} c= (B \ D) \/ {x} by XBOOLE_1:7;
hence contradiction by A4, A9, A31, A29, TARSKI:def_4; ::_thesis: verum
end;
hence y in union B ; ::_thesis: verum
end;
hence union B = Y by XBOOLE_0:def_10; ::_thesis: verum
end;
Lm3: now__::_thesis:_for_Y_being_set_
for_H_being_Hierarchy_of_Y
for_B_being_mutually-disjoint_Subset-Family_of_Y_st_B_c=_H_&_(_for_C_being_mutually-disjoint_Subset-Family_of_Y_st_C_c=_H_&_union_B_c=_union_C_holds_
B_=_C_)_holds_
for_S1_being_Subset_of_Y_st_S1_in_B_holds_
S1_<>_{}
let Y be set ; ::_thesis: for H being Hierarchy of Y
for B being mutually-disjoint Subset-Family of Y st B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds
B = C ) holds
for S1 being Subset of Y st S1 in B holds
S1 <> {}
let H be Hierarchy of Y; ::_thesis: for B being mutually-disjoint Subset-Family of Y st B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds
B = C ) holds
for S1 being Subset of Y st S1 in B holds
S1 <> {}
let B be mutually-disjoint Subset-Family of Y; ::_thesis: ( B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds
B = C ) implies for S1 being Subset of Y st S1 in B holds
S1 <> {} )
assume that
A1: B c= H and
A2: for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds
B = C ; ::_thesis: for S1 being Subset of Y st S1 in B holds
S1 <> {}
let S1 be Subset of Y; ::_thesis: ( S1 in B implies S1 <> {} )
assume A3: S1 in B ; ::_thesis: S1 <> {}
now__::_thesis:_not_S1_=_{}
set C = B \ {{}};
assume A4: S1 = {} ; ::_thesis: contradiction
A5: union B c= union (B \ {{}})
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union B or x in union (B \ {{}}) )
assume x in union B ; ::_thesis: x in union (B \ {{}})
then consider y being set such that
A6: x in y and
A7: y in B by TARSKI:def_4;
not y in {{}} by A6, TARSKI:def_1;
then y in B \ {{}} by A7, XBOOLE_0:def_5;
hence x in union (B \ {{}}) by A6, TARSKI:def_4; ::_thesis: verum
end;
A8: B \ {{}} is mutually-disjoint
proof
let x, y be set ; :: according to TAXONOM2:def_5 ::_thesis: ( x in B \ {{}} & y in B \ {{}} & x <> y implies x misses y )
assume that
A9: x in B \ {{}} and
A10: y in B \ {{}} and
A11: x <> y ; ::_thesis: x misses y
A12: y in B by A10, XBOOLE_0:def_5;
x in B by A9, XBOOLE_0:def_5;
hence x misses y by A11, A12, Def5; ::_thesis: verum
end;
B \ {{}} c= B by XBOOLE_1:36;
then B \ {{}} c= H by A1, XBOOLE_1:1;
then B = B \ {{}} by A2, A5, A8;
then not {} in {{}} by A3, A4, XBOOLE_0:def_5;
hence contradiction by TARSKI:def_1; ::_thesis: verum
end;
hence S1 <> {} ; ::_thesis: verum
end;
definition
let Y be set ;
let F be Subset-Family of Y;
attrF is T_3 means :Def6: :: TAXONOM2:def 6
for A being Subset of Y st A in F holds
for x being Element of Y st not x in A holds
ex B being Subset of Y st
( x in B & B in F & A misses B );
end;
:: deftheorem Def6 defines T_3 TAXONOM2:def_6_:_
for Y being set
for F being Subset-Family of Y holds
( F is T_3 iff for A being Subset of Y st A in F holds
for x being Element of Y st not x in A holds
ex B being Subset of Y st
( x in B & B in F & A misses B ) );
theorem Th11: :: TAXONOM2:11
for Y being set
for F being Subset-Family of Y st F = {} holds
F is T_3
proof
let Y be set ; ::_thesis: for F being Subset-Family of Y st F = {} holds
F is T_3
let F be Subset-Family of Y; ::_thesis: ( F = {} implies F is T_3 )
assume A1: F = {} ; ::_thesis: F is T_3
let A be Subset of Y; :: according to TAXONOM2:def_6 ::_thesis: ( A in F implies for x being Element of Y st not x in A holds
ex B being Subset of Y st
( x in B & B in F & A misses B ) )
assume A2: A in F ; ::_thesis: for x being Element of Y st not x in A holds
ex B being Subset of Y st
( x in B & B in F & A misses B )
let x be Element of Y; ::_thesis: ( not x in A implies ex B being Subset of Y st
( x in B & B in F & A misses B ) )
assume not x in A ; ::_thesis: ex B being Subset of Y st
( x in B & B in F & A misses B )
thus ex B being Subset of Y st
( x in B & B in F & A misses B ) by A1, A2; ::_thesis: verum
end;
registration
let Y be set ;
cluster covering T_3 for Hierarchy of Y;
existence
ex b1 being Hierarchy of Y st
( b1 is covering & b1 is T_3 )
proof
percases ( Y <> {} or Y = {} ) ;
supposeA1: Y <> {} ; ::_thesis: ex b1 being Hierarchy of Y st
( b1 is covering & b1 is T_3 )
set H9 = {Y};
reconsider H = {Y} as Subset-Family of Y by ZFMISC_1:68;
H is hierarchic
proof
let x, y be set ; :: according to TAXONOM2:def_3 ::_thesis: ( x in H & y in H & not x c= y & not y c= x implies x misses y )
assume that
A2: x in H and
A3: y in H ; ::_thesis: ( x c= y or y c= x or x misses y )
x = Y by A2, TARSKI:def_1;
hence ( x c= y or y c= x or x misses y ) by A3; ::_thesis: verum
end;
then reconsider H = H as Hierarchy of Y by Def4;
take H ; ::_thesis: ( H is covering & H is T_3 )
union H = Y by ZFMISC_1:25;
hence H is covering by ABIAN:4; ::_thesis: H is T_3
thus H is T_3 ::_thesis: verum
proof
let A be Subset of Y; :: according to TAXONOM2:def_6 ::_thesis: ( A in H implies for x being Element of Y st not x in A holds
ex B being Subset of Y st
( x in B & B in H & A misses B ) )
assume A in H ; ::_thesis: for x being Element of Y st not x in A holds
ex B being Subset of Y st
( x in B & B in H & A misses B )
then A4: A = Y by TARSKI:def_1;
let x be Element of Y; ::_thesis: ( not x in A implies ex B being Subset of Y st
( x in B & B in H & A misses B ) )
assume not x in A ; ::_thesis: ex B being Subset of Y st
( x in B & B in H & A misses B )
hence ex B being Subset of Y st
( x in B & B in H & A misses B ) by A1, A4; ::_thesis: verum
end;
end;
supposeA5: Y = {} ; ::_thesis: ex b1 being Hierarchy of Y st
( b1 is covering & b1 is T_3 )
set H9 = {} ;
reconsider H = {} as Subset-Family of Y by XBOOLE_1:2;
reconsider H1 = H as Hierarchy of Y by Def4, Th6;
take H1 ; ::_thesis: ( H1 is covering & H1 is T_3 )
thus H1 is covering by A5, ABIAN:4, ZFMISC_1:2; ::_thesis: H1 is T_3
thus H1 is T_3 by Th11; ::_thesis: verum
end;
end;
end;
end;
definition
let Y be set ;
let F be Subset-Family of Y;
attrF is lower-bounded means :Def7: :: TAXONOM2:def 7
for B being set st B <> {} & B c= F & B is c=-linear holds
ex c being set st
( c in F & c c= meet B );
end;
:: deftheorem Def7 defines lower-bounded TAXONOM2:def_7_:_
for Y being set
for F being Subset-Family of Y holds
( F is lower-bounded iff for B being set st B <> {} & B c= F & B is c=-linear holds
ex c being set st
( c in F & c c= meet B ) );
theorem Th12: :: TAXONOM2:12
for Y being set
for S1 being Subset of Y
for B being mutually-disjoint Subset-Family of Y st ( for b being set st b in B holds
( S1 misses b & Y <> {} ) ) holds
( B \/ {S1} is mutually-disjoint Subset-Family of Y & ( S1 <> {} implies union (B \/ {S1}) <> union B ) )
proof
let Y be set ; ::_thesis: for S1 being Subset of Y
for B being mutually-disjoint Subset-Family of Y st ( for b being set st b in B holds
( S1 misses b & Y <> {} ) ) holds
( B \/ {S1} is mutually-disjoint Subset-Family of Y & ( S1 <> {} implies union (B \/ {S1}) <> union B ) )
let S1 be Subset of Y; ::_thesis: for B being mutually-disjoint Subset-Family of Y st ( for b being set st b in B holds
( S1 misses b & Y <> {} ) ) holds
( B \/ {S1} is mutually-disjoint Subset-Family of Y & ( S1 <> {} implies union (B \/ {S1}) <> union B ) )
let B be mutually-disjoint Subset-Family of Y; ::_thesis: ( ( for b being set st b in B holds
( S1 misses b & Y <> {} ) ) implies ( B \/ {S1} is mutually-disjoint Subset-Family of Y & ( S1 <> {} implies union (B \/ {S1}) <> union B ) ) )
assume A1: for b being set st b in B holds
( S1 misses b & Y <> {} ) ; ::_thesis: ( B \/ {S1} is mutually-disjoint Subset-Family of Y & ( S1 <> {} implies union (B \/ {S1}) <> union B ) )
set C = B \/ {S1};
A2: now__::_thesis:_for_c1,_c2_being_set_st_c1_in_B_\/_{S1}_&_c2_in_B_\/_{S1}_&_c1_<>_c2_holds_
c1_misses_c2
let c1, c2 be set ; ::_thesis: ( c1 in B \/ {S1} & c2 in B \/ {S1} & c1 <> c2 implies b1 misses b2 )
assume that
A3: c1 in B \/ {S1} and
A4: c2 in B \/ {S1} and
A5: c1 <> c2 ; ::_thesis: b1 misses b2
percases ( c1 in B or c1 in {S1} ) by A3, XBOOLE_0:def_3;
supposeA6: c1 in B ; ::_thesis: b1 misses b2
percases ( c2 in B or c2 in {S1} ) by A4, XBOOLE_0:def_3;
suppose c2 in B ; ::_thesis: b1 misses b2
hence c1 misses c2 by A5, A6, Def5; ::_thesis: verum
end;
suppose c2 in {S1} ; ::_thesis: b1 misses b2
then c2 = S1 by TARSKI:def_1;
hence c1 misses c2 by A1, A6; ::_thesis: verum
end;
end;
end;
suppose c1 in {S1} ; ::_thesis: b1 misses b2
then A7: c1 = S1 by TARSKI:def_1;
then not c2 in {S1} by A5, TARSKI:def_1;
then c2 in B by A4, XBOOLE_0:def_3;
hence c1 misses c2 by A1, A7; ::_thesis: verum
end;
end;
end;
{S1} c= bool Y
proof
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in {S1} or p in bool Y )
assume p in {S1} ; ::_thesis: p in bool Y
then p = S1 by TARSKI:def_1;
hence p in bool Y ; ::_thesis: verum
end;
hence B \/ {S1} is mutually-disjoint Subset-Family of Y by A2, Def5, XBOOLE_1:8; ::_thesis: ( S1 <> {} implies union (B \/ {S1}) <> union B )
thus ( S1 <> {} implies union (B \/ {S1}) <> union B ) ::_thesis: verum
proof
assume A8: S1 <> {} ; ::_thesis: union (B \/ {S1}) <> union B
not union (B \/ {S1}) c= union B
proof
A9: {S1} c= B \/ {S1} by XBOOLE_1:7;
assume A10: union (B \/ {S1}) c= union B ; ::_thesis: contradiction
consider p being set such that
A11: p in S1 by A8, XBOOLE_0:def_1;
S1 in {S1} by TARSKI:def_1;
then p in union (B \/ {S1}) by A11, A9, TARSKI:def_4;
then consider S2 being set such that
A12: p in S2 and
A13: S2 in B by A10, TARSKI:def_4;
S1 misses S2 by A1, A13;
hence contradiction by A11, A12, XBOOLE_0:3; ::_thesis: verum
end;
hence union (B \/ {S1}) <> union B ; ::_thesis: verum
end;
end;
definition
let Y be set ;
let F be Subset-Family of Y;
attrF is with_max's means :Def8: :: TAXONOM2:def 8
for S being Subset of Y st S in F holds
ex T being Subset of Y st
( S c= T & T in F & ( for V being Subset of Y st T c= V & V in F holds
V = Y ) );
end;
:: deftheorem Def8 defines with_max's TAXONOM2:def_8_:_
for Y being set
for F being Subset-Family of Y holds
( F is with_max's iff for S being Subset of Y st S in F holds
ex T being Subset of Y st
( S c= T & T in F & ( for V being Subset of Y st T c= V & V in F holds
V = Y ) ) );
begin
theorem :: TAXONOM2:13
for Y being set
for H being covering Hierarchy of Y st H is with_max's holds
ex P being a_partition of Y st P c= H
proof
let Y be set ; ::_thesis: for H being covering Hierarchy of Y st H is with_max's holds
ex P being a_partition of Y st P c= H
let H be covering Hierarchy of Y; ::_thesis: ( H is with_max's implies ex P being a_partition of Y st P c= H )
assume A1: H is with_max's ; ::_thesis: ex P being a_partition of Y st P c= H
percases ( Y = {} or Y <> {} ) ;
supposeA2: Y = {} ; ::_thesis: ex P being a_partition of Y st P c= H
set P9 = {} ;
reconsider P = {} as Subset-Family of Y by XBOOLE_1:2;
take P ; ::_thesis: ( P is a_partition of Y & P c= H )
thus ( P is a_partition of Y & P c= H ) by A2, EQREL_1:45, XBOOLE_1:2; ::_thesis: verum
end;
supposeA3: Y <> {} ; ::_thesis: ex P being a_partition of Y st P c= H
now__::_thesis:_ex_P_being_a_partition_of_Y_st_P_c=_H
percases ( Y in H or not Y in H ) ;
supposeA4: Y in H ; ::_thesis: ex P being a_partition of Y st P c= H
set P = {Y};
A5: {Y} c= H
proof
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in {Y} or p in H )
assume p in {Y} ; ::_thesis: p in H
hence p in H by A4, TARSKI:def_1; ::_thesis: verum
end;
{Y} is a_partition of Y by A3, EQREL_1:39;
hence ex P being a_partition of Y st P c= H by A5; ::_thesis: verum
end;
supposeA6: not Y in H ; ::_thesis: ex P being a_partition of Y st P c= H
defpred S1[ set ] means ex S being Subset of Y st
( S in H & S c= $1 & ( for V being Subset of Y st $1 c= V & V in H holds
V = Y ) );
consider P9 being set such that
A7: for T being set holds
( T in P9 iff ( T in H & S1[T] ) ) from XBOOLE_0:sch_1();
A8: P9 c= H
proof
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in P9 or p in H )
assume p in P9 ; ::_thesis: p in H
hence p in H by A7; ::_thesis: verum
end;
then reconsider P = P9 as Subset-Family of Y by XBOOLE_1:1;
A9: now__::_thesis:_for_S1_being_Subset_of_Y_st_S1_in_P_holds_
(_S1_<>_{}_&_(_for_S2_being_Subset_of_Y_holds_
(_not_S2_in_P_or_S1_=_S2_or_S1_misses_S2_)_)_)
let S1 be Subset of Y; ::_thesis: ( S1 in P implies ( S1 <> {} & ( for S2 being Subset of Y holds
( not S2 in P or S1 = S2 or S1 misses S2 ) ) ) )
assume A10: S1 in P ; ::_thesis: ( S1 <> {} & ( for S2 being Subset of Y holds
( not S2 in P or S1 = S2 or S1 misses S2 ) ) )
thus S1 <> {} ::_thesis: for S2 being Subset of Y holds
( not S2 in P or S1 = S2 or S1 misses S2 )
proof
consider S being Subset of Y such that
A11: S in H and
A12: S c= S1 and
A13: for V being Subset of Y st S1 c= V & V in H holds
V = Y by A7, A10;
assume A14: S1 = {} ; ::_thesis: contradiction
then S1 = S by A12
.= Y by A14, A11, A13, XBOOLE_1:2 ;
hence contradiction by A3, A14; ::_thesis: verum
end;
thus for S2 being Subset of Y holds
( not S2 in P or S1 = S2 or S1 misses S2 ) ::_thesis: verum
proof
let S2 be Subset of Y; ::_thesis: ( not S2 in P or S1 = S2 or S1 misses S2 )
assume A15: S2 in P ; ::_thesis: ( S1 = S2 or S1 misses S2 )
A16: ex T being Subset of Y st
( T in H & T c= S2 & ( for V being Subset of Y st S2 c= V & V in H holds
V = Y ) ) by A7, A15;
S2 in H by A7, A15;
hence ( S1 = S2 or S1 misses S2 ) by A6, A16; ::_thesis: verum
end;
end;
A17: union H = Y by ABIAN:4;
Y c= union P
proof
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in Y or p in union P )
assume p in Y ; ::_thesis: p in union P
then consider h9 being set such that
A18: p in h9 and
A19: h9 in H by A17, TARSKI:def_4;
reconsider h = h9 as Subset of Y by A19;
consider T being Subset of Y such that
A20: h c= T and
A21: T in H and
A22: for V being Subset of Y st T c= V & V in H holds
V = Y by A1, A19, Def8;
T in P by A7, A21, A22;
hence p in union P by A18, A20, TARSKI:def_4; ::_thesis: verum
end;
then union P = Y by XBOOLE_0:def_10;
then P is a_partition of Y by A9, EQREL_1:def_4;
hence ex P being a_partition of Y st P c= H by A8; ::_thesis: verum
end;
end;
end;
hence ex P being a_partition of Y st P c= H ; ::_thesis: verum
end;
end;
end;
theorem :: TAXONOM2:14
for Y being set
for H being covering Hierarchy of Y
for B being mutually-disjoint Subset-Family of Y st B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds
B = C ) holds
B is a_partition of Y
proof
let Y be set ; ::_thesis: for H being covering Hierarchy of Y
for B being mutually-disjoint Subset-Family of Y st B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds
B = C ) holds
B is a_partition of Y
let H be covering Hierarchy of Y; ::_thesis: for B being mutually-disjoint Subset-Family of Y st B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds
B = C ) holds
B is a_partition of Y
let B be mutually-disjoint Subset-Family of Y; ::_thesis: ( B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds
B = C ) implies B is a_partition of Y )
assume that
A1: B c= H and
A2: for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds
B = C ; ::_thesis: B is a_partition of Y
thus union B = Y by A1, A2, Lm2; :: according to EQREL_1:def_4 ::_thesis: for b1 being Element of bool Y holds
( not b1 in B or ( not b1 = {} & ( for b2 being Element of bool Y holds
( not b2 in B or b1 = b2 or b1 misses b2 ) ) ) )
thus for b1 being Element of bool Y holds
( not b1 in B or ( not b1 = {} & ( for b2 being Element of bool Y holds
( not b2 in B or b1 = b2 or b1 misses b2 ) ) ) ) by A1, A2, Def5, Lm3; ::_thesis: verum
end;
theorem :: TAXONOM2:15
for Y being set
for H being covering T_3 Hierarchy of Y st H is lower-bounded & not {} in H holds
for A being Subset of Y
for B being mutually-disjoint Subset-Family of Y st A in B & B c= H & ( for C being mutually-disjoint Subset-Family of Y st A in C & C c= H & union B c= union C holds
union B = union C ) holds
B is a_partition of Y
proof
let Y be set ; ::_thesis: for H being covering T_3 Hierarchy of Y st H is lower-bounded & not {} in H holds
for A being Subset of Y
for B being mutually-disjoint Subset-Family of Y st A in B & B c= H & ( for C being mutually-disjoint Subset-Family of Y st A in C & C c= H & union B c= union C holds
union B = union C ) holds
B is a_partition of Y
let H be covering T_3 Hierarchy of Y; ::_thesis: ( H is lower-bounded & not {} in H implies for A being Subset of Y
for B being mutually-disjoint Subset-Family of Y st A in B & B c= H & ( for C being mutually-disjoint Subset-Family of Y st A in C & C c= H & union B c= union C holds
union B = union C ) holds
B is a_partition of Y )
assume that
A1: H is lower-bounded and
A2: not {} in H ; ::_thesis: for A being Subset of Y
for B being mutually-disjoint Subset-Family of Y st A in B & B c= H & ( for C being mutually-disjoint Subset-Family of Y st A in C & C c= H & union B c= union C holds
union B = union C ) holds
B is a_partition of Y
let A be Subset of Y; ::_thesis: for B being mutually-disjoint Subset-Family of Y st A in B & B c= H & ( for C being mutually-disjoint Subset-Family of Y st A in C & C c= H & union B c= union C holds
union B = union C ) holds
B is a_partition of Y
let B be mutually-disjoint Subset-Family of Y; ::_thesis: ( A in B & B c= H & ( for C being mutually-disjoint Subset-Family of Y st A in C & C c= H & union B c= union C holds
union B = union C ) implies B is a_partition of Y )
assume that
A3: A in B and
A4: B c= H and
A5: for C being mutually-disjoint Subset-Family of Y st A in C & C c= H & union B c= union C holds
union B = union C ; ::_thesis: B is a_partition of Y
A6: union H = Y by ABIAN:4;
A7: H is hierarchic by Def4;
percases ( Y <> {} or Y = {} ) ;
supposeA8: Y <> {} ; ::_thesis: B is a_partition of Y
Y c= union B
proof
assume not Y c= union B ; ::_thesis: contradiction
then consider x being set such that
A9: x in Y and
A10: not x in union B by TARSKI:def_3;
consider xx being set such that
A11: x in xx and
A12: xx in H by A6, A9, TARSKI:def_4;
defpred S1[ set ] means x in $1;
consider D being set such that
A13: for h being set holds
( h in D iff ( h in H & S1[h] ) ) from XBOOLE_0:sch_1();
A14: D c= H
proof
let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in D or d in H )
assume d in D ; ::_thesis: d in H
hence d in H by A13; ::_thesis: verum
end;
now__::_thesis:_for_h1,_h2_being_set_st_h1_in_D_&_h2_in_D_holds_
h1,h2_are_c=-comparable
let h1, h2 be set ; ::_thesis: ( h1 in D & h2 in D implies h1,h2 are_c=-comparable )
assume that
A15: h1 in D and
A16: h2 in D ; ::_thesis: h1,h2 are_c=-comparable
now__::_thesis:_not_h1_misses_h2
A17: x in h2 by A13, A16;
assume A18: h1 misses h2 ; ::_thesis: contradiction
x in h1 by A13, A15;
hence contradiction by A18, A17, XBOOLE_0:3; ::_thesis: verum
end;
then ( h1 c= h2 or h2 c= h1 ) by A7, A14, A15, A16, Def3;
hence h1,h2 are_c=-comparable by XBOOLE_0:def_9; ::_thesis: verum
end;
then A19: D is c=-linear by ORDINAL1:def_8;
xx in D by A13, A11, A12;
then consider min1 being set such that
A20: min1 in H and
A21: min1 c= meet D by A1, A14, A19, Def7;
reconsider min9 = min1 as Subset of Y by A20;
set C = B \/ {min9};
A22: B c= B \/ {min9} by XBOOLE_1:7;
now__::_thesis:_for_b1_being_set_st_b1_in_B_holds_
b1_misses_min9
reconsider x9 = x as Element of Y by A9;
let b1 be set ; ::_thesis: ( b1 in B implies b1 misses min9 )
assume A23: b1 in B ; ::_thesis: b1 misses min9
reconsider b19 = b1 as Subset of Y by A23;
A24: not x9 in b19 by A10, A23, TARSKI:def_4;
A25: not b1 c= min9
proof
reconsider b19 = b1 as Subset of Y by A23;
consider k being Subset of Y such that
A26: x9 in k and
A27: k in H and
A28: k misses b19 by A4, A23, A24, Def6;
k in D by A13, A26, A27;
then meet D c= k by SETFAM_1:3;
then A29: min9 c= k by A21, XBOOLE_1:1;
b1 <> {} by A2, A4, A23;
then A30: ex y being set st y in b19 by XBOOLE_0:def_1;
assume b1 c= min9 ; ::_thesis: contradiction
then b19 c= k by A29, XBOOLE_1:1;
hence contradiction by A28, A30, XBOOLE_0:3; ::_thesis: verum
end;
not min9 c= b1
proof
consider k being Subset of Y such that
A31: x9 in k and
A32: k in H and
A33: k misses b19 by A4, A23, A24, Def6;
k in D by A13, A31, A32;
then meet D c= k by SETFAM_1:3;
then A34: min9 c= k by A21, XBOOLE_1:1;
assume A35: min9 c= b1 ; ::_thesis: contradiction
ex y being set st y in min9 by A2, A20, XBOOLE_0:def_1;
hence contradiction by A35, A33, A34, XBOOLE_0:3; ::_thesis: verum
end;
hence b1 misses min9 by A4, A7, A20, A23, A25, Def3; ::_thesis: verum
end;
then A36: for b being set st b in B holds
( min9 misses b & Y <> {} ) by A8;
then A37: B \/ {min9} is mutually-disjoint Subset-Family of Y by Th12;
{min9} c= H
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in {min9} or s in H )
assume s in {min9} ; ::_thesis: s in H
hence s in H by A20, TARSKI:def_1; ::_thesis: verum
end;
then A38: B \/ {min9} c= H by A4, XBOOLE_1:8;
union (B \/ {min9}) <> union B by A2, A20, A36, Th12;
hence contradiction by A3, A5, A37, A38, A22, ZFMISC_1:77; ::_thesis: verum
end;
then A39: union B = Y by XBOOLE_0:def_10;
for A being Subset of Y st A in B holds
( A <> {} & ( for E being Subset of Y holds
( not E in B or A = E or A misses E ) ) ) by A2, A4, Def5;
hence B is a_partition of Y by A39, EQREL_1:def_4; ::_thesis: verum
end;
supposeA40: Y = {} ; ::_thesis: B is a_partition of Y
now__::_thesis:_B_=_{}
percases ( H = {} or H = {{}} ) by A40, ZFMISC_1:1, ZFMISC_1:33;
suppose H = {} ; ::_thesis: B = {}
hence B = {} by A4; ::_thesis: verum
end;
supposeA41: H = {{}} ; ::_thesis: B = {}
B <> {{}}
proof
assume B = {{}} ; ::_thesis: contradiction
then {} in B by TARSKI:def_1;
hence contradiction by A2, A4; ::_thesis: verum
end;
hence B = {} by A4, A41, ZFMISC_1:33; ::_thesis: verum
end;
end;
end;
hence B is a_partition of Y by A40, EQREL_1:45; ::_thesis: verum
end;
end;
end;
theorem Th16: :: TAXONOM2:16
for Y being set
for H being covering T_3 Hierarchy of Y st H is lower-bounded & not {} in H holds
for A being Subset of Y
for B being mutually-disjoint Subset-Family of Y st A in B & B c= H & ( for C being mutually-disjoint Subset-Family of Y st A in C & C c= H & B c= C holds
B = C ) holds
B is a_partition of Y
proof
let Y be set ; ::_thesis: for H being covering T_3 Hierarchy of Y st H is lower-bounded & not {} in H holds
for A being Subset of Y
for B being mutually-disjoint Subset-Family of Y st A in B & B c= H & ( for C being mutually-disjoint Subset-Family of Y st A in C & C c= H & B c= C holds
B = C ) holds
B is a_partition of Y
let H be covering T_3 Hierarchy of Y; ::_thesis: ( H is lower-bounded & not {} in H implies for A being Subset of Y
for B being mutually-disjoint Subset-Family of Y st A in B & B c= H & ( for C being mutually-disjoint Subset-Family of Y st A in C & C c= H & B c= C holds
B = C ) holds
B is a_partition of Y )
assume that
A1: H is lower-bounded and
A2: not {} in H ; ::_thesis: for A being Subset of Y
for B being mutually-disjoint Subset-Family of Y st A in B & B c= H & ( for C being mutually-disjoint Subset-Family of Y st A in C & C c= H & B c= C holds
B = C ) holds
B is a_partition of Y
let A be Subset of Y; ::_thesis: for B being mutually-disjoint Subset-Family of Y st A in B & B c= H & ( for C being mutually-disjoint Subset-Family of Y st A in C & C c= H & B c= C holds
B = C ) holds
B is a_partition of Y
let B be mutually-disjoint Subset-Family of Y; ::_thesis: ( A in B & B c= H & ( for C being mutually-disjoint Subset-Family of Y st A in C & C c= H & B c= C holds
B = C ) implies B is a_partition of Y )
assume that
A3: A in B and
A4: B c= H and
A5: for C being mutually-disjoint Subset-Family of Y st A in C & C c= H & B c= C holds
B = C ; ::_thesis: B is a_partition of Y
A6: union H = Y by ABIAN:4;
A7: H is hierarchic by Def4;
percases ( Y <> {} or Y = {} ) ;
supposeA8: Y <> {} ; ::_thesis: B is a_partition of Y
Y c= union B
proof
assume not Y c= union B ; ::_thesis: contradiction
then consider x being set such that
A9: x in Y and
A10: not x in union B by TARSKI:def_3;
consider xx being set such that
A11: x in xx and
A12: xx in H by A6, A9, TARSKI:def_4;
defpred S1[ set ] means x in $1;
consider D being set such that
A13: for h being set holds
( h in D iff ( h in H & S1[h] ) ) from XBOOLE_0:sch_1();
A14: D c= H
proof
let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in D or d in H )
assume d in D ; ::_thesis: d in H
hence d in H by A13; ::_thesis: verum
end;
now__::_thesis:_for_h1,_h2_being_set_st_h1_in_D_&_h2_in_D_holds_
h1,h2_are_c=-comparable
let h1, h2 be set ; ::_thesis: ( h1 in D & h2 in D implies h1,h2 are_c=-comparable )
assume that
A15: h1 in D and
A16: h2 in D ; ::_thesis: h1,h2 are_c=-comparable
now__::_thesis:_not_h1_misses_h2
A17: x in h2 by A13, A16;
assume A18: h1 misses h2 ; ::_thesis: contradiction
x in h1 by A13, A15;
hence contradiction by A18, A17, XBOOLE_0:3; ::_thesis: verum
end;
then ( h1 c= h2 or h2 c= h1 ) by A7, A14, A15, A16, Def3;
hence h1,h2 are_c=-comparable by XBOOLE_0:def_9; ::_thesis: verum
end;
then A19: D is c=-linear by ORDINAL1:def_8;
xx in D by A13, A11, A12;
then consider min1 being set such that
A20: min1 in H and
A21: min1 c= meet D by A1, A14, A19, Def7;
reconsider min9 = min1 as Subset of Y by A20;
A22: {min9} c= H
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in {min9} or s in H )
assume s in {min9} ; ::_thesis: s in H
hence s in H by A20, TARSKI:def_1; ::_thesis: verum
end;
set C = B \/ {min9};
now__::_thesis:_for_b1_being_set_st_b1_in_B_holds_
b1_misses_min9
reconsider x9 = x as Element of Y by A9;
let b1 be set ; ::_thesis: ( b1 in B implies b1 misses min9 )
assume A23: b1 in B ; ::_thesis: b1 misses min9
reconsider b19 = b1 as Subset of Y by A23;
A24: not x9 in b19 by A10, A23, TARSKI:def_4;
A25: not b1 c= min9
proof
reconsider b19 = b1 as Subset of Y by A23;
consider k being Subset of Y such that
A26: x9 in k and
A27: k in H and
A28: k misses b19 by A4, A23, A24, Def6;
k in D by A13, A26, A27;
then meet D c= k by SETFAM_1:3;
then A29: min9 c= k by A21, XBOOLE_1:1;
b1 <> {} by A2, A4, A23;
then A30: ex y being set st y in b19 by XBOOLE_0:def_1;
assume b1 c= min9 ; ::_thesis: contradiction
then b19 c= k by A29, XBOOLE_1:1;
hence contradiction by A28, A30, XBOOLE_0:3; ::_thesis: verum
end;
not min9 c= b1
proof
consider k being Subset of Y such that
A31: x9 in k and
A32: k in H and
A33: k misses b19 by A4, A23, A24, Def6;
k in D by A13, A31, A32;
then meet D c= k by SETFAM_1:3;
then A34: min9 c= k by A21, XBOOLE_1:1;
assume A35: min9 c= b1 ; ::_thesis: contradiction
ex y being set st y in min9 by A2, A20, XBOOLE_0:def_1;
hence contradiction by A35, A33, A34, XBOOLE_0:3; ::_thesis: verum
end;
hence b1 misses min9 by A4, A7, A20, A23, A25, Def3; ::_thesis: verum
end;
then A36: for b being set st b in B holds
( min9 misses b & Y <> {} ) by A8;
then A37: B \/ {min9} is mutually-disjoint Subset-Family of Y by Th12;
A38: B c= B \/ {min9} by XBOOLE_1:7;
union (B \/ {min9}) <> union B by A2, A20, A36, Th12;
hence contradiction by A3, A4, A5, A37, A22, A38, XBOOLE_1:8; ::_thesis: verum
end;
then A39: union B = Y by XBOOLE_0:def_10;
for A being Subset of Y st A in B holds
( A <> {} & ( for E being Subset of Y holds
( not E in B or A = E or A misses E ) ) ) by A2, A4, Def5;
hence B is a_partition of Y by A39, EQREL_1:def_4; ::_thesis: verum
end;
supposeA40: Y = {} ; ::_thesis: B is a_partition of Y
now__::_thesis:_B_=_{}
percases ( H = {} or H = {{}} ) by A40, ZFMISC_1:1, ZFMISC_1:33;
suppose H = {} ; ::_thesis: B = {}
hence B = {} by A4; ::_thesis: verum
end;
supposeA41: H = {{}} ; ::_thesis: B = {}
B <> {{}}
proof
assume B = {{}} ; ::_thesis: contradiction
then {} in B by TARSKI:def_1;
hence contradiction by A2, A4; ::_thesis: verum
end;
hence B = {} by A4, A41, ZFMISC_1:33; ::_thesis: verum
end;
end;
end;
hence B is a_partition of Y by A40, EQREL_1:45; ::_thesis: verum
end;
end;
end;
theorem Th17: :: TAXONOM2:17
for Y being set
for H being covering T_3 Hierarchy of Y st H is lower-bounded & not {} in H holds
for A being Subset of Y st A in H holds
ex P being a_partition of Y st
( A in P & P c= H )
proof
let Y be set ; ::_thesis: for H being covering T_3 Hierarchy of Y st H is lower-bounded & not {} in H holds
for A being Subset of Y st A in H holds
ex P being a_partition of Y st
( A in P & P c= H )
let H be covering T_3 Hierarchy of Y; ::_thesis: ( H is lower-bounded & not {} in H implies for A being Subset of Y st A in H holds
ex P being a_partition of Y st
( A in P & P c= H ) )
assume that
A1: H is lower-bounded and
A2: not {} in H ; ::_thesis: for A being Subset of Y st A in H holds
ex P being a_partition of Y st
( A in P & P c= H )
let A be Subset of Y; ::_thesis: ( A in H implies ex P being a_partition of Y st
( A in P & P c= H ) )
assume A3: A in H ; ::_thesis: ex P being a_partition of Y st
( A in P & P c= H )
set k1 = {A};
A4: {A} c= H by A3, ZFMISC_1:31;
A5: A in {A} by TARSKI:def_1;
A6: {A} c= bool Y by ZFMISC_1:31;
defpred S1[ set ] means ( A in $1 & $1 is mutually-disjoint & $1 c= H );
consider K being set such that
A7: for S being set holds
( S in K iff ( S in bool (bool Y) & S1[S] ) ) from XBOOLE_0:sch_1();
{A} is mutually-disjoint by Th10;
then A8: {A} in K by A7, A5, A4, A6;
for Z being set st Z c= K & Z is c=-linear holds
ex X3 being set st
( X3 in K & ( for X1 being set st X1 in Z holds
X1 c= X3 ) )
proof
let Z be set ; ::_thesis: ( Z c= K & Z is c=-linear implies ex X3 being set st
( X3 in K & ( for X1 being set st X1 in Z holds
X1 c= X3 ) ) )
assume that
A9: Z c= K and
A10: Z is c=-linear ; ::_thesis: ex X3 being set st
( X3 in K & ( for X1 being set st X1 in Z holds
X1 c= X3 ) )
A11: now__::_thesis:_for_X1,_X2_being_set_st_X1_in_Z_&_X2_in_Z_&_not_X1_c=_X2_holds_
X2_c=_X1
let X1, X2 be set ; ::_thesis: ( X1 in Z & X2 in Z & not X1 c= X2 implies X2 c= X1 )
assume that
A12: X1 in Z and
A13: X2 in Z ; ::_thesis: ( X1 c= X2 or X2 c= X1 )
X1,X2 are_c=-comparable by A10, A12, A13, ORDINAL1:def_8;
hence ( X1 c= X2 or X2 c= X1 ) by XBOOLE_0:def_9; ::_thesis: verum
end;
percases ( Z <> {} or Z = {} ) ;
supposeA14: Z <> {} ; ::_thesis: ex X3 being set st
( X3 in K & ( for X1 being set st X1 in Z holds
X1 c= X3 ) )
set X3 = union Z;
take union Z ; ::_thesis: ( union Z in K & ( for X1 being set st X1 in Z holds
X1 c= union Z ) )
now__::_thesis:_(_A_in_union_Z_&_union_Z_in_bool_(bool_Y)_&_union_Z_is_mutually-disjoint_&_union_Z_c=_H_)
consider z being set such that
A15: z in Z by A14, XBOOLE_0:def_1;
A in z by A7, A9, A15;
hence A in union Z by A15, TARSKI:def_4; ::_thesis: ( union Z in bool (bool Y) & union Z is mutually-disjoint & union Z c= H )
A16: for a being set st a in Z holds
a c= H by A7, A9;
then union Z c= H by ZFMISC_1:76;
then union Z c= bool Y by XBOOLE_1:1;
hence union Z in bool (bool Y) ; ::_thesis: ( union Z is mutually-disjoint & union Z c= H )
thus union Z is mutually-disjoint ::_thesis: union Z c= H
proof
let t1, t2 be set ; :: according to TAXONOM2:def_5 ::_thesis: ( t1 in union Z & t2 in union Z & t1 <> t2 implies t1 misses t2 )
assume that
A17: t1 in union Z and
A18: t2 in union Z and
A19: t1 <> t2 ; ::_thesis: t1 misses t2
consider v1 being set such that
A20: t1 in v1 and
A21: v1 in Z by A17, TARSKI:def_4;
A22: v1 is mutually-disjoint by A7, A9, A21;
consider v2 being set such that
A23: t2 in v2 and
A24: v2 in Z by A18, TARSKI:def_4;
A25: v2 is mutually-disjoint by A7, A9, A24;
percases ( v1 c= v2 or v2 c= v1 ) by A11, A21, A24;
suppose v1 c= v2 ; ::_thesis: t1 misses t2
hence t1 misses t2 by A19, A20, A23, A25, Def5; ::_thesis: verum
end;
suppose v2 c= v1 ; ::_thesis: t1 misses t2
hence t1 misses t2 by A19, A20, A23, A22, Def5; ::_thesis: verum
end;
end;
end;
thus union Z c= H by A16, ZFMISC_1:76; ::_thesis: verum
end;
hence union Z in K by A7; ::_thesis: for X1 being set st X1 in Z holds
X1 c= union Z
thus for X1 being set st X1 in Z holds
X1 c= union Z by ZFMISC_1:74; ::_thesis: verum
end;
supposeA26: Z = {} ; ::_thesis: ex X3 being set st
( X3 in K & ( for X1 being set st X1 in Z holds
X1 c= X3 ) )
consider a being set such that
A27: a in K by A8;
take a ; ::_thesis: ( a in K & ( for X1 being set st X1 in Z holds
X1 c= a ) )
thus a in K by A27; ::_thesis: for X1 being set st X1 in Z holds
X1 c= a
thus for X1 being set st X1 in Z holds
X1 c= a by A26; ::_thesis: verum
end;
end;
end;
then consider M being set such that
A28: M in K and
A29: for Z being set st Z in K & Z <> M holds
not M c= Z by A8, ORDERS_1:65;
A30: M is mutually-disjoint Subset-Family of Y by A7, A28;
A31: now__::_thesis:_for_C_being_mutually-disjoint_Subset-Family_of_Y_st_A_in_C_&_C_c=_H_&_M_c=_C_holds_
M_=_C
let C be mutually-disjoint Subset-Family of Y; ::_thesis: ( A in C & C c= H & M c= C implies M = C )
assume that
A32: A in C and
A33: C c= H and
A34: M c= C ; ::_thesis: M = C
C in K by A7, A32, A33;
hence M = C by A29, A34; ::_thesis: verum
end;
A35: A in M by A7, A28;
take M ; ::_thesis: ( M is Element of bool (bool Y) & M is a_partition of Y & A in M & M c= H )
M c= H by A7, A28;
hence ( M is Element of bool (bool Y) & M is a_partition of Y & A in M & M c= H ) by A1, A2, A30, A35, A31, Th16; ::_thesis: verum
end;
Lm4: now__::_thesis:_for_x_being_non_empty_set_
for_y_being_set_st_x_c=_y_holds_
x_meets_y
let x be non empty set ; ::_thesis: for y being set st x c= y holds
x meets y
A1: ex a being set st a in x by XBOOLE_0:def_1;
let y be set ; ::_thesis: ( x c= y implies x meets y )
assume x c= y ; ::_thesis: x meets y
hence x meets y by A1, XBOOLE_0:3; ::_thesis: verum
end;
theorem Th18: :: TAXONOM2:18
for X, h being non empty set
for Pmin being a_partition of X
for hw being set st hw in Pmin & h c= hw holds
for PS being a_partition of X st h in PS & ( for x being set holds
( not x in PS or x c= hw or hw c= x or hw misses x ) ) holds
for PT being set st ( for a being set holds
( a in PT iff ( a in PS & a c= hw ) ) ) holds
( PT \/ (Pmin \ {hw}) is a_partition of X & PT \/ (Pmin \ {hw}) is_finer_than Pmin )
proof
let X, h be non empty set ; ::_thesis: for Pmin being a_partition of X
for hw being set st hw in Pmin & h c= hw holds
for PS being a_partition of X st h in PS & ( for x being set holds
( not x in PS or x c= hw or hw c= x or hw misses x ) ) holds
for PT being set st ( for a being set holds
( a in PT iff ( a in PS & a c= hw ) ) ) holds
( PT \/ (Pmin \ {hw}) is a_partition of X & PT \/ (Pmin \ {hw}) is_finer_than Pmin )
let Pmin be a_partition of X; ::_thesis: for hw being set st hw in Pmin & h c= hw holds
for PS being a_partition of X st h in PS & ( for x being set holds
( not x in PS or x c= hw or hw c= x or hw misses x ) ) holds
for PT being set st ( for a being set holds
( a in PT iff ( a in PS & a c= hw ) ) ) holds
( PT \/ (Pmin \ {hw}) is a_partition of X & PT \/ (Pmin \ {hw}) is_finer_than Pmin )
let hw be set ; ::_thesis: ( hw in Pmin & h c= hw implies for PS being a_partition of X st h in PS & ( for x being set holds
( not x in PS or x c= hw or hw c= x or hw misses x ) ) holds
for PT being set st ( for a being set holds
( a in PT iff ( a in PS & a c= hw ) ) ) holds
( PT \/ (Pmin \ {hw}) is a_partition of X & PT \/ (Pmin \ {hw}) is_finer_than Pmin ) )
assume that
A1: hw in Pmin and
A2: h c= hw ; ::_thesis: for PS being a_partition of X st h in PS & ( for x being set holds
( not x in PS or x c= hw or hw c= x or hw misses x ) ) holds
for PT being set st ( for a being set holds
( a in PT iff ( a in PS & a c= hw ) ) ) holds
( PT \/ (Pmin \ {hw}) is a_partition of X & PT \/ (Pmin \ {hw}) is_finer_than Pmin )
let PS be a_partition of X; ::_thesis: ( h in PS & ( for x being set holds
( not x in PS or x c= hw or hw c= x or hw misses x ) ) implies for PT being set st ( for a being set holds
( a in PT iff ( a in PS & a c= hw ) ) ) holds
( PT \/ (Pmin \ {hw}) is a_partition of X & PT \/ (Pmin \ {hw}) is_finer_than Pmin ) )
assume that
A3: h in PS and
A4: for x being set holds
( not x in PS or x c= hw or hw c= x or hw misses x ) ; ::_thesis: for PT being set st ( for a being set holds
( a in PT iff ( a in PS & a c= hw ) ) ) holds
( PT \/ (Pmin \ {hw}) is a_partition of X & PT \/ (Pmin \ {hw}) is_finer_than Pmin )
let PT be set ; ::_thesis: ( ( for a being set holds
( a in PT iff ( a in PS & a c= hw ) ) ) implies ( PT \/ (Pmin \ {hw}) is a_partition of X & PT \/ (Pmin \ {hw}) is_finer_than Pmin ) )
assume A5: for a being set holds
( a in PT iff ( a in PS & a c= hw ) ) ; ::_thesis: ( PT \/ (Pmin \ {hw}) is a_partition of X & PT \/ (Pmin \ {hw}) is_finer_than Pmin )
A6: PT c= PS
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in PT or a in PS )
assume a in PT ; ::_thesis: a in PS
hence a in PS by A5; ::_thesis: verum
end;
A7: union PS = X by EQREL_1:def_4;
A8: union Pmin = X by EQREL_1:def_4;
set P = PT \/ (Pmin \ {hw});
A9: PT c= PT \/ (Pmin \ {hw}) by XBOOLE_1:7;
A10: Pmin \ {hw} c= PT \/ (Pmin \ {hw}) by XBOOLE_1:7;
A11: h in PT by A2, A3, A5;
A12: X c= union (PT \/ (Pmin \ {hw}))
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X or a in union (PT \/ (Pmin \ {hw})) )
assume A13: a in X ; ::_thesis: a in union (PT \/ (Pmin \ {hw}))
consider b being set such that
A14: a in b and
A15: b in Pmin by A8, A13, TARSKI:def_4;
percases ( b = hw or b <> hw ) ;
supposeA16: b = hw ; ::_thesis: a in union (PT \/ (Pmin \ {hw}))
consider c being set such that
A17: a in c and
A18: c in PS by A7, A13, TARSKI:def_4;
A19: hw meets c by A14, A16, A17, XBOOLE_0:3;
percases ( hw c= c or c c= hw ) by A4, A18, A19;
suppose hw c= c ; ::_thesis: a in union (PT \/ (Pmin \ {hw}))
then A20: h c= c by A2, XBOOLE_1:1;
h meets c
proof
A21: ex x being set st x in h by XBOOLE_0:def_1;
assume h misses c ; ::_thesis: contradiction
hence contradiction by A20, A21, XBOOLE_0:3; ::_thesis: verum
end;
then h = c by A3, A18, EQREL_1:def_4;
hence a in union (PT \/ (Pmin \ {hw})) by A9, A11, A17, TARSKI:def_4; ::_thesis: verum
end;
suppose c c= hw ; ::_thesis: a in union (PT \/ (Pmin \ {hw}))
then c in PT by A5, A18;
hence a in union (PT \/ (Pmin \ {hw})) by A9, A17, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
suppose b <> hw ; ::_thesis: a in union (PT \/ (Pmin \ {hw}))
then not b in {hw} by TARSKI:def_1;
then b in Pmin \ {hw} by A15, XBOOLE_0:def_5;
hence a in union (PT \/ (Pmin \ {hw})) by A10, A14, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
A22: Pmin \ {hw} c= Pmin by XBOOLE_1:36;
A23: now__::_thesis:_for_x,_y_being_set_st_x_in_PT_&_y_in_Pmin_\_{hw}_holds_
x_misses_y
let x, y be set ; ::_thesis: ( x in PT & y in Pmin \ {hw} implies x misses y )
assume that
A24: x in PT and
A25: y in Pmin \ {hw} ; ::_thesis: x misses y
A26: y in Pmin by A25, XBOOLE_0:def_5;
not y in {hw} by A25, XBOOLE_0:def_5;
then A27: y <> hw by TARSKI:def_1;
A28: x c= hw by A5, A24;
now__::_thesis:_not_x_meets_y
assume x meets y ; ::_thesis: contradiction
then ex a being set st
( a in x & a in y ) by XBOOLE_0:3;
then hw meets y by A28, XBOOLE_0:3;
hence contradiction by A1, A26, A27, EQREL_1:def_4; ::_thesis: verum
end;
hence x misses y ; ::_thesis: verum
end;
A29: now__::_thesis:_for_A_being_Subset_of_X_st_A_in_PT_\/_(Pmin_\_{hw})_holds_
(_A_<>_{}_&_(_for_B_being_Subset_of_X_holds_
(_not_B_in_PT_\/_(Pmin_\_{hw})_or_A_=_B_or_A_misses_B_)_)_)
let A be Subset of X; ::_thesis: ( A in PT \/ (Pmin \ {hw}) implies ( A <> {} & ( for B being Subset of X holds
( not B in PT \/ (Pmin \ {hw}) or A = B or A misses B ) ) ) )
assume A30: A in PT \/ (Pmin \ {hw}) ; ::_thesis: ( A <> {} & ( for B being Subset of X holds
( not B in PT \/ (Pmin \ {hw}) or A = B or A misses B ) ) )
now__::_thesis:_A_<>_{}
percases ( A in PT or A in Pmin \ {hw} ) by A30, XBOOLE_0:def_3;
suppose A in PT ; ::_thesis: A <> {}
hence A <> {} by A6, EQREL_1:def_4; ::_thesis: verum
end;
suppose A in Pmin \ {hw} ; ::_thesis: A <> {}
hence A <> {} by A22, EQREL_1:def_4; ::_thesis: verum
end;
end;
end;
hence A <> {} ; ::_thesis: for B being Subset of X holds
( not B in PT \/ (Pmin \ {hw}) or A = B or A misses B )
thus for B being Subset of X holds
( not B in PT \/ (Pmin \ {hw}) or A = B or A misses B ) ::_thesis: verum
proof
let B be Subset of X; ::_thesis: ( not B in PT \/ (Pmin \ {hw}) or A = B or A misses B )
assume A31: B in PT \/ (Pmin \ {hw}) ; ::_thesis: ( A = B or A misses B )
percases ( A in PT or A in Pmin \ {hw} ) by A30, XBOOLE_0:def_3;
supposeA32: A in PT ; ::_thesis: ( A = B or A misses B )
percases ( B in PT or B in Pmin \ {hw} ) by A31, XBOOLE_0:def_3;
suppose B in PT ; ::_thesis: ( A = B or A misses B )
hence ( A = B or A misses B ) by A6, A32, EQREL_1:def_4; ::_thesis: verum
end;
suppose B in Pmin \ {hw} ; ::_thesis: ( A = B or A misses B )
hence ( A = B or A misses B ) by A23, A32; ::_thesis: verum
end;
end;
end;
supposeA33: A in Pmin \ {hw} ; ::_thesis: ( A = B or A misses B )
percases ( B in PT or B in Pmin \ {hw} ) by A31, XBOOLE_0:def_3;
suppose B in PT ; ::_thesis: ( A = B or A misses B )
hence ( A = B or A misses B ) by A23, A33; ::_thesis: verum
end;
suppose B in Pmin \ {hw} ; ::_thesis: ( A = B or A misses B )
hence ( A = B or A misses B ) by A22, A33, EQREL_1:def_4; ::_thesis: verum
end;
end;
end;
end;
end;
end;
PT c= bool X by A6, XBOOLE_1:1;
then A34: PT \/ (Pmin \ {hw}) c= bool X by XBOOLE_1:8;
union (PT \/ (Pmin \ {hw})) c= X
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in union (PT \/ (Pmin \ {hw})) or a in X )
assume a in union (PT \/ (Pmin \ {hw})) ; ::_thesis: a in X
then ex b being set st
( a in b & b in PT \/ (Pmin \ {hw}) ) by TARSKI:def_4;
hence a in X by A34; ::_thesis: verum
end;
then union (PT \/ (Pmin \ {hw})) = X by A12, XBOOLE_0:def_10;
hence PT \/ (Pmin \ {hw}) is a_partition of X by A34, A29, EQREL_1:def_4; ::_thesis: PT \/ (Pmin \ {hw}) is_finer_than Pmin
let a be set ; :: according to SETFAM_1:def_2 ::_thesis: ( not a in PT \/ (Pmin \ {hw}) or ex b1 being set st
( b1 in Pmin & a c= b1 ) )
assume A35: a in PT \/ (Pmin \ {hw}) ; ::_thesis: ex b1 being set st
( b1 in Pmin & a c= b1 )
percases ( a in PT or a in Pmin \ {hw} ) by A35, XBOOLE_0:def_3;
suppose a in PT ; ::_thesis: ex b1 being set st
( b1 in Pmin & a c= b1 )
then a c= hw by A5;
hence ex b1 being set st
( b1 in Pmin & a c= b1 ) by A1; ::_thesis: verum
end;
suppose a in Pmin \ {hw} ; ::_thesis: ex b1 being set st
( b1 in Pmin & a c= b1 )
hence ex b1 being set st
( b1 in Pmin & a c= b1 ) by A22; ::_thesis: verum
end;
end;
end;
theorem Th19: :: TAXONOM2:19
for X, h being non empty set st h c= X holds
for Pmax being a_partition of X st ex hy being set st
( hy in Pmax & hy c= h ) & ( for x being set holds
( not x in Pmax or x c= h or h c= x or h misses x ) ) holds
for Pb being set st ( for x being set holds
( x in Pb iff ( x in Pmax & x misses h ) ) ) holds
( Pb \/ {h} is a_partition of X & Pmax is_finer_than Pb \/ {h} & ( for Pmin being a_partition of X st Pmax is_finer_than Pmin holds
for hw being set st hw in Pmin & h c= hw holds
Pb \/ {h} is_finer_than Pmin ) )
proof
let X, h be non empty set ; ::_thesis: ( h c= X implies for Pmax being a_partition of X st ex hy being set st
( hy in Pmax & hy c= h ) & ( for x being set holds
( not x in Pmax or x c= h or h c= x or h misses x ) ) holds
for Pb being set st ( for x being set holds
( x in Pb iff ( x in Pmax & x misses h ) ) ) holds
( Pb \/ {h} is a_partition of X & Pmax is_finer_than Pb \/ {h} & ( for Pmin being a_partition of X st Pmax is_finer_than Pmin holds
for hw being set st hw in Pmin & h c= hw holds
Pb \/ {h} is_finer_than Pmin ) ) )
assume A1: h c= X ; ::_thesis: for Pmax being a_partition of X st ex hy being set st
( hy in Pmax & hy c= h ) & ( for x being set holds
( not x in Pmax or x c= h or h c= x or h misses x ) ) holds
for Pb being set st ( for x being set holds
( x in Pb iff ( x in Pmax & x misses h ) ) ) holds
( Pb \/ {h} is a_partition of X & Pmax is_finer_than Pb \/ {h} & ( for Pmin being a_partition of X st Pmax is_finer_than Pmin holds
for hw being set st hw in Pmin & h c= hw holds
Pb \/ {h} is_finer_than Pmin ) )
A2: {h} c= bool X
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in {h} or s in bool X )
assume s in {h} ; ::_thesis: s in bool X
then s = h by TARSKI:def_1;
hence s in bool X by A1; ::_thesis: verum
end;
A3: h in {h} by TARSKI:def_1;
let Pmax be a_partition of X; ::_thesis: ( ex hy being set st
( hy in Pmax & hy c= h ) & ( for x being set holds
( not x in Pmax or x c= h or h c= x or h misses x ) ) implies for Pb being set st ( for x being set holds
( x in Pb iff ( x in Pmax & x misses h ) ) ) holds
( Pb \/ {h} is a_partition of X & Pmax is_finer_than Pb \/ {h} & ( for Pmin being a_partition of X st Pmax is_finer_than Pmin holds
for hw being set st hw in Pmin & h c= hw holds
Pb \/ {h} is_finer_than Pmin ) ) )
assume that
A4: ex hy being set st
( hy in Pmax & hy c= h ) and
A5: for x being set holds
( not x in Pmax or x c= h or h c= x or h misses x ) ; ::_thesis: for Pb being set st ( for x being set holds
( x in Pb iff ( x in Pmax & x misses h ) ) ) holds
( Pb \/ {h} is a_partition of X & Pmax is_finer_than Pb \/ {h} & ( for Pmin being a_partition of X st Pmax is_finer_than Pmin holds
for hw being set st hw in Pmin & h c= hw holds
Pb \/ {h} is_finer_than Pmin ) )
A6: now__::_thesis:_for_s_being_set_st_s_in_Pmax_&_h_c=_s_holds_
h_=_s
let s be set ; ::_thesis: ( s in Pmax & h c= s implies h = s )
assume that
A7: s in Pmax and
A8: h c= s ; ::_thesis: h = s
consider hy being set such that
A9: hy in Pmax and
A10: hy c= h by A4;
hy <> {} by A9, EQREL_1:def_4;
then hy meets s by A8, A10, Lm4, XBOOLE_1:1;
then s = hy by A7, A9, EQREL_1:def_4;
hence h = s by A8, A10, XBOOLE_0:def_10; ::_thesis: verum
end;
let Pb be set ; ::_thesis: ( ( for x being set holds
( x in Pb iff ( x in Pmax & x misses h ) ) ) implies ( Pb \/ {h} is a_partition of X & Pmax is_finer_than Pb \/ {h} & ( for Pmin being a_partition of X st Pmax is_finer_than Pmin holds
for hw being set st hw in Pmin & h c= hw holds
Pb \/ {h} is_finer_than Pmin ) ) )
assume A11: for x being set holds
( x in Pb iff ( x in Pmax & x misses h ) ) ; ::_thesis: ( Pb \/ {h} is a_partition of X & Pmax is_finer_than Pb \/ {h} & ( for Pmin being a_partition of X st Pmax is_finer_than Pmin holds
for hw being set st hw in Pmin & h c= hw holds
Pb \/ {h} is_finer_than Pmin ) )
set P = Pb \/ {h};
A12: Pb c= Pb \/ {h} by XBOOLE_1:7;
A13: Pb c= Pmax
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in Pb or s in Pmax )
assume s in Pb ; ::_thesis: s in Pmax
hence s in Pmax by A11; ::_thesis: verum
end;
A14: now__::_thesis:_for_A_being_Subset_of_X_st_A_in_Pb_\/_{h}_holds_
(_A_<>_{}_&_(_for_B_being_Subset_of_X_holds_
(_not_B_in_Pb_\/_{h}_or_A_=_B_or_A_misses_B_)_)_)
let A be Subset of X; ::_thesis: ( A in Pb \/ {h} implies ( A <> {} & ( for B being Subset of X holds
( not B in Pb \/ {h} or A = B or A misses B ) ) ) )
assume A15: A in Pb \/ {h} ; ::_thesis: ( A <> {} & ( for B being Subset of X holds
( not B in Pb \/ {h} or A = B or A misses B ) ) )
now__::_thesis:_A_<>_{}
percases ( A in Pb or A in {h} ) by A15, XBOOLE_0:def_3;
suppose A in Pb ; ::_thesis: A <> {}
then A in Pmax by A11;
hence A <> {} by EQREL_1:def_4; ::_thesis: verum
end;
suppose A in {h} ; ::_thesis: A <> {}
hence A <> {} by TARSKI:def_1; ::_thesis: verum
end;
end;
end;
hence A <> {} ; ::_thesis: for B being Subset of X holds
( not B in Pb \/ {h} or A = B or A misses B )
thus for B being Subset of X holds
( not B in Pb \/ {h} or A = B or A misses B ) ::_thesis: verum
proof
let B be Subset of X; ::_thesis: ( not B in Pb \/ {h} or A = B or A misses B )
assume A16: B in Pb \/ {h} ; ::_thesis: ( A = B or A misses B )
percases ( A in Pb or A in {h} ) by A15, XBOOLE_0:def_3;
supposeA17: A in Pb ; ::_thesis: ( A = B or A misses B )
percases ( B in Pb or B in {h} ) by A16, XBOOLE_0:def_3;
suppose B in Pb ; ::_thesis: ( A = B or A misses B )
hence ( A = B or A misses B ) by A13, A17, EQREL_1:def_4; ::_thesis: verum
end;
suppose B in {h} ; ::_thesis: ( A = B or A misses B )
then B = h by TARSKI:def_1;
hence ( A = B or A misses B ) by A11, A17; ::_thesis: verum
end;
end;
end;
supposeA18: A in {h} ; ::_thesis: ( A = B or A misses B )
percases ( B in Pb or B in {h} ) by A16, XBOOLE_0:def_3;
supposeA19: B in Pb ; ::_thesis: ( A = B or A misses B )
A = h by A18, TARSKI:def_1;
hence ( A = B or A misses B ) by A11, A19; ::_thesis: verum
end;
suppose B in {h} ; ::_thesis: ( A = B or A misses B )
then B = h by TARSKI:def_1;
hence ( A = B or A misses B ) by A18, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
end;
end;
end;
A20: {h} c= Pb \/ {h} by XBOOLE_1:7;
A21: union Pmax = X by EQREL_1:def_4;
A22: X c= union (Pb \/ {h})
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in X or s in union (Pb \/ {h}) )
assume s in X ; ::_thesis: s in union (Pb \/ {h})
then consider t being set such that
A23: s in t and
A24: t in Pmax by A21, TARSKI:def_4;
percases ( t in Pb or not t in Pb ) ;
suppose t in Pb ; ::_thesis: s in union (Pb \/ {h})
hence s in union (Pb \/ {h}) by A12, A23, TARSKI:def_4; ::_thesis: verum
end;
suppose not t in Pb ; ::_thesis: s in union (Pb \/ {h})
then A25: t meets h by A11, A24;
percases ( h c= t or t c= h ) by A5, A24, A25;
suppose h c= t ; ::_thesis: s in union (Pb \/ {h})
then t = h by A6, A24;
hence s in union (Pb \/ {h}) by A3, A20, A23, TARSKI:def_4; ::_thesis: verum
end;
supposeA26: t c= h ; ::_thesis: s in union (Pb \/ {h})
h in {h} by TARSKI:def_1;
hence s in union (Pb \/ {h}) by A20, A23, A26, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
end;
end;
Pb c= bool X by A13, XBOOLE_1:1;
then A27: Pb \/ {h} c= bool X by A2, XBOOLE_1:8;
union (Pb \/ {h}) c= X
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in union (Pb \/ {h}) or s in X )
assume s in union (Pb \/ {h}) ; ::_thesis: s in X
then ex t being set st
( s in t & t in Pb \/ {h} ) by TARSKI:def_4;
hence s in X by A27; ::_thesis: verum
end;
then union (Pb \/ {h}) = X by A22, XBOOLE_0:def_10;
hence Pb \/ {h} is a_partition of X by A27, A14, EQREL_1:def_4; ::_thesis: ( Pmax is_finer_than Pb \/ {h} & ( for Pmin being a_partition of X st Pmax is_finer_than Pmin holds
for hw being set st hw in Pmin & h c= hw holds
Pb \/ {h} is_finer_than Pmin ) )
thus Pmax is_finer_than Pb \/ {h} ::_thesis: for Pmin being a_partition of X st Pmax is_finer_than Pmin holds
for hw being set st hw in Pmin & h c= hw holds
Pb \/ {h} is_finer_than Pmin
proof
let x be set ; :: according to SETFAM_1:def_2 ::_thesis: ( not x in Pmax or ex b1 being set st
( b1 in Pb \/ {h} & x c= b1 ) )
assume A28: x in Pmax ; ::_thesis: ex b1 being set st
( b1 in Pb \/ {h} & x c= b1 )
percases ( x c= h or not x c= h ) ;
suppose x c= h ; ::_thesis: ex b1 being set st
( b1 in Pb \/ {h} & x c= b1 )
hence ex b1 being set st
( b1 in Pb \/ {h} & x c= b1 ) by A3, A20; ::_thesis: verum
end;
supposeA29: not x c= h ; ::_thesis: ex b1 being set st
( b1 in Pb \/ {h} & x c= b1 )
percases ( h c= x or h misses x ) by A5, A28, A29;
suppose h c= x ; ::_thesis: ex b1 being set st
( b1 in Pb \/ {h} & x c= b1 )
then h = x by A6, A28;
hence ex b1 being set st
( b1 in Pb \/ {h} & x c= b1 ) by A3, A20; ::_thesis: verum
end;
suppose h misses x ; ::_thesis: ex b1 being set st
( b1 in Pb \/ {h} & x c= b1 )
then x in Pb by A11, A28;
hence ex b1 being set st
( b1 in Pb \/ {h} & x c= b1 ) by A12; ::_thesis: verum
end;
end;
end;
end;
end;
let Pmin be a_partition of X; ::_thesis: ( Pmax is_finer_than Pmin implies for hw being set st hw in Pmin & h c= hw holds
Pb \/ {h} is_finer_than Pmin )
assume A30: Pmax is_finer_than Pmin ; ::_thesis: for hw being set st hw in Pmin & h c= hw holds
Pb \/ {h} is_finer_than Pmin
let hw be set ; ::_thesis: ( hw in Pmin & h c= hw implies Pb \/ {h} is_finer_than Pmin )
assume that
A31: hw in Pmin and
A32: h c= hw ; ::_thesis: Pb \/ {h} is_finer_than Pmin
let s be set ; :: according to SETFAM_1:def_2 ::_thesis: ( not s in Pb \/ {h} or ex b1 being set st
( b1 in Pmin & s c= b1 ) )
assume A33: s in Pb \/ {h} ; ::_thesis: ex b1 being set st
( b1 in Pmin & s c= b1 )
percases ( s in Pb or s in {h} ) by A33, XBOOLE_0:def_3;
suppose s in Pb ; ::_thesis: ex b1 being set st
( b1 in Pmin & s c= b1 )
then s in Pmax by A11;
hence ex b1 being set st
( b1 in Pmin & s c= b1 ) by A30, SETFAM_1:def_2; ::_thesis: verum
end;
suppose s in {h} ; ::_thesis: ex b1 being set st
( b1 in Pmin & s c= b1 )
then s = h by TARSKI:def_1;
hence ex b1 being set st
( b1 in Pmin & s c= b1 ) by A31, A32; ::_thesis: verum
end;
end;
end;
theorem :: TAXONOM2:20
for X being non empty set
for H being covering T_3 Hierarchy of X st H is lower-bounded & not {} in H & ( for C1 being set st C1 <> {} & C1 c= PARTITIONS X & ( for P1, P2 being set st P1 in C1 & P2 in C1 & not P1 is_finer_than P2 holds
P2 is_finer_than P1 ) holds
ex PX, PY being set st
( PX in C1 & PY in C1 & ( for PZ being set st PZ in C1 holds
( PZ is_finer_than PY & PX is_finer_than PZ ) ) ) ) holds
ex C being Classification of X st union C = H
proof
let X be non empty set ; ::_thesis: for H being covering T_3 Hierarchy of X st H is lower-bounded & not {} in H & ( for C1 being set st C1 <> {} & C1 c= PARTITIONS X & ( for P1, P2 being set st P1 in C1 & P2 in C1 & not P1 is_finer_than P2 holds
P2 is_finer_than P1 ) holds
ex PX, PY being set st
( PX in C1 & PY in C1 & ( for PZ being set st PZ in C1 holds
( PZ is_finer_than PY & PX is_finer_than PZ ) ) ) ) holds
ex C being Classification of X st union C = H
let H be covering T_3 Hierarchy of X; ::_thesis: ( H is lower-bounded & not {} in H & ( for C1 being set st C1 <> {} & C1 c= PARTITIONS X & ( for P1, P2 being set st P1 in C1 & P2 in C1 & not P1 is_finer_than P2 holds
P2 is_finer_than P1 ) holds
ex PX, PY being set st
( PX in C1 & PY in C1 & ( for PZ being set st PZ in C1 holds
( PZ is_finer_than PY & PX is_finer_than PZ ) ) ) ) implies ex C being Classification of X st union C = H )
assume that
A1: H is lower-bounded and
A2: not {} in H and
A3: for C1 being set st C1 <> {} & C1 c= PARTITIONS X & ( for P1, P2 being set st P1 in C1 & P2 in C1 & not P1 is_finer_than P2 holds
P2 is_finer_than P1 ) holds
ex PX, PY being set st
( PX in C1 & PY in C1 & ( for PZ being set st PZ in C1 holds
( PZ is_finer_than PY & PX is_finer_than PZ ) ) ) ; ::_thesis: ex C being Classification of X st union C = H
union H = X by ABIAN:4;
then consider h being set such that
A4: h in H by XBOOLE_0:def_1, ZFMISC_1:2;
reconsider h = h as Subset of X by A4;
consider PX being a_partition of X such that
h in PX and
A5: PX c= H by A1, A2, A4, Th17;
set L = {PX};
A6: {PX} c= PARTITIONS X
proof
let l be set ; :: according to TARSKI:def_3 ::_thesis: ( not l in {PX} or l in PARTITIONS X )
assume l in {PX} ; ::_thesis: l in PARTITIONS X
then l = PX by TARSKI:def_1;
hence l in PARTITIONS X by PARTIT1:def_3; ::_thesis: verum
end;
A7: now__::_thesis:_for_P1,_P2_being_set_st_P1_in_{PX}_&_P2_in_{PX}_&_not_P1_is_finer_than_P2_holds_
P2_is_finer_than_P1
let P1, P2 be set ; ::_thesis: ( P1 in {PX} & P2 in {PX} & not P1 is_finer_than P2 implies P2 is_finer_than P1 )
assume that
A8: P1 in {PX} and
A9: P2 in {PX} ; ::_thesis: ( P1 is_finer_than P2 or P2 is_finer_than P1 )
P1 = PX by A8, TARSKI:def_1;
hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A9, TARSKI:def_1; ::_thesis: verum
end;
A10: H is hierarchic by Def4;
defpred S1[ set ] means ( ( for P being set st P in $1 holds
P c= H ) & ( for P1, P2 being set st P1 in $1 & P2 in $1 & not P1 is_finer_than P2 holds
P2 is_finer_than P1 ) );
consider RL being set such that
A11: for L being set holds
( L in RL iff ( L in bool (PARTITIONS X) & S1[L] ) ) from XBOOLE_0:sch_1();
for a being set st a in {PX} holds
a c= H by A5, TARSKI:def_1;
then A12: {PX} in RL by A11, A6, A7;
now__::_thesis:_for_Z_being_set_st_Z_c=_RL_&_Z_is_c=-linear_holds_
ex_Y_being_set_st_
(_Y_in_RL_&_(_for_X1_being_set_st_X1_in_Z_holds_
X1_c=_Y_)_)
let Z be set ; ::_thesis: ( Z c= RL & Z is c=-linear implies ex Y being set st
( Y in RL & ( for X1 being set st X1 in Z holds
X1 c= Y ) ) )
assume that
A13: Z c= RL and
A14: Z is c=-linear ; ::_thesis: ex Y being set st
( Y in RL & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
set Y = union Z;
A15: now__::_thesis:_for_X1,_X2_being_set_st_X1_in_Z_&_X2_in_Z_&_not_X1_c=_X2_holds_
X2_c=_X1
let X1, X2 be set ; ::_thesis: ( X1 in Z & X2 in Z & not X1 c= X2 implies X2 c= X1 )
assume that
A16: X1 in Z and
A17: X2 in Z ; ::_thesis: ( X1 c= X2 or X2 c= X1 )
X1,X2 are_c=-comparable by A14, A16, A17, ORDINAL1:def_8;
hence ( X1 c= X2 or X2 c= X1 ) by XBOOLE_0:def_9; ::_thesis: verum
end;
A18: now__::_thesis:_for_P1,_P2_being_set_st_P1_in_union_Z_&_P2_in_union_Z_&_not_P1_is_finer_than_P2_holds_
P2_is_finer_than_P1
let P1, P2 be set ; ::_thesis: ( P1 in union Z & P2 in union Z & not b1 is_finer_than b2 implies b2 is_finer_than b1 )
assume that
A19: P1 in union Z and
A20: P2 in union Z ; ::_thesis: ( b1 is_finer_than b2 or b2 is_finer_than b1 )
consider L1 being set such that
A21: P1 in L1 and
A22: L1 in Z by A19, TARSKI:def_4;
consider L2 being set such that
A23: P2 in L2 and
A24: L2 in Z by A20, TARSKI:def_4;
percases ( L1 c= L2 or L2 c= L1 ) by A15, A22, A24;
suppose L1 c= L2 ; ::_thesis: ( b1 is_finer_than b2 or b2 is_finer_than b1 )
hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A11, A13, A21, A23, A24; ::_thesis: verum
end;
suppose L2 c= L1 ; ::_thesis: ( b1 is_finer_than b2 or b2 is_finer_than b1 )
hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A11, A13, A21, A22, A23; ::_thesis: verum
end;
end;
end;
take Y = union Z; ::_thesis: ( Y in RL & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
A25: now__::_thesis:_for_P_being_set_st_P_in_Y_holds_
P_c=_H
let P be set ; ::_thesis: ( P in Y implies P c= H )
assume P in Y ; ::_thesis: P c= H
then ex L3 being set st
( P in L3 & L3 in Z ) by TARSKI:def_4;
hence P c= H by A11, A13; ::_thesis: verum
end;
Y c= PARTITIONS X
proof
let P be set ; :: according to TARSKI:def_3 ::_thesis: ( not P in Y or P in PARTITIONS X )
assume P in Y ; ::_thesis: P in PARTITIONS X
then consider L4 being set such that
A26: P in L4 and
A27: L4 in Z by TARSKI:def_4;
L4 in bool (PARTITIONS X) by A11, A13, A27;
hence P in PARTITIONS X by A26; ::_thesis: verum
end;
hence Y in RL by A11, A25, A18; ::_thesis: for X1 being set st X1 in Z holds
X1 c= Y
thus for X1 being set st X1 in Z holds
X1 c= Y by ZFMISC_1:74; ::_thesis: verum
end;
then consider C being set such that
A28: C in RL and
A29: for Z being set st Z in RL & Z <> C holds
not C c= Z by A12, ORDERS_1:65;
reconsider C = C as Subset of (PARTITIONS X) by A11, A28;
A30: C is Classification of X
proof
let P1, P2 be a_partition of X; :: according to TAXONOM1:def_1 ::_thesis: ( not P1 in C or not P2 in C or P1 is_finer_than P2 or P2 is_finer_than P1 )
assume that
A31: P1 in C and
A32: P2 in C ; ::_thesis: ( P1 is_finer_than P2 or P2 is_finer_than P1 )
thus ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A11, A28, A31, A32; ::_thesis: verum
end;
A33: C <> {} by A12, A29, XBOOLE_1:2;
A34: H c= union C
proof
let h be set ; :: according to TARSKI:def_3 ::_thesis: ( not h in H or h in union C )
assume A35: h in H ; ::_thesis: h in union C
percases ( not h in union C or h in union C ) ;
supposeA36: not h in union C ; ::_thesis: h in union C
defpred S2[ set ] means ex hx being set st
( hx in $1 & h c= hx & h <> hx );
consider Ca being set such that
A37: for p being set holds
( p in Ca iff ( p in C & S2[p] ) ) from XBOOLE_0:sch_1();
A38: Ca c= C
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in Ca or s in C )
assume s in Ca ; ::_thesis: s in C
hence s in C by A37; ::_thesis: verum
end;
defpred S3[ set ] means ex hx being set st
( hx in $1 & hx c= h & h <> hx );
consider Cb being set such that
A39: for p being set holds
( p in Cb iff ( p in C & S3[p] ) ) from XBOOLE_0:sch_1();
consider PS being a_partition of X such that
A40: h in PS and
A41: PS c= H by A1, A2, A35, Th17;
A42: h <> {} by A40, EQREL_1:def_4;
A43: now__::_thesis:_for_p_being_set_st_p_in_C_holds_
ex_hv_being_set_st_
(_hv_in_p_&_not_hv_misses_h_)
consider t being set such that
A44: t in h by A42, XBOOLE_0:def_1;
let p be set ; ::_thesis: ( p in C implies ex hv being set st
( hv in p & not hv misses h ) )
assume p in C ; ::_thesis: ex hv being set st
( hv in p & not hv misses h )
then p is a_partition of X by PARTIT1:def_3;
then union p = X by EQREL_1:def_4;
then consider v being set such that
A45: t in v and
A46: v in p by A35, A44, TARSKI:def_4;
assume A47: for hv being set st hv in p holds
hv misses h ; ::_thesis: contradiction
not v misses h by A44, A45, XBOOLE_0:3;
hence contradiction by A47, A46; ::_thesis: verum
end;
A48: C c= Ca \/ Cb
proof
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in C or p in Ca \/ Cb )
assume A49: p in C ; ::_thesis: p in Ca \/ Cb
consider hv being set such that
A50: hv in p and
A51: not hv misses h by A43, A49;
A52: h <> hv by A36, A49, A50, TARSKI:def_4;
A53: p c= H by A11, A28, A49;
percases ( hv c= h or h c= hv ) by A10, A35, A50, A51, A53, Def3;
suppose hv c= h ; ::_thesis: p in Ca \/ Cb
then p in Cb by A39, A49, A50, A52;
hence p in Ca \/ Cb by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose h c= hv ; ::_thesis: p in Ca \/ Cb
then p in Ca by A37, A49, A50, A52;
hence p in Ca \/ Cb by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
Cb c= C
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in Cb or s in C )
assume s in Cb ; ::_thesis: s in C
hence s in C by A39; ::_thesis: verum
end;
then Ca \/ Cb c= C by A38, XBOOLE_1:8;
then A54: C = Ca \/ Cb by A48, XBOOLE_0:def_10;
then A55: Ca c= C by XBOOLE_1:7;
A56: now__::_thesis:_for_P1,_P2_being_set_st_P1_in_Ca_&_P2_in_Ca_&_not_P1_is_finer_than_P2_holds_
P2_is_finer_than_P1
let P1, P2 be set ; ::_thesis: ( P1 in Ca & P2 in Ca & not P1 is_finer_than P2 implies P2 is_finer_than P1 )
assume that
A57: P1 in Ca and
A58: P2 in Ca ; ::_thesis: ( P1 is_finer_than P2 or P2 is_finer_than P1 )
P2 in C by A55, A58;
then A59: P2 is a_partition of X by PARTIT1:def_3;
P1 in C by A55, A57;
then P1 is a_partition of X by PARTIT1:def_3;
hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A30, A55, A57, A58, A59, TAXONOM1:def_1; ::_thesis: verum
end;
A60: Cb c= C by A54, XBOOLE_1:7;
A61: now__::_thesis:_for_P1,_P2_being_set_st_P1_in_Cb_&_P2_in_Cb_&_not_P1_is_finer_than_P2_holds_
P2_is_finer_than_P1
let P1, P2 be set ; ::_thesis: ( P1 in Cb & P2 in Cb & not P1 is_finer_than P2 implies P2 is_finer_than P1 )
assume that
A62: P1 in Cb and
A63: P2 in Cb ; ::_thesis: ( P1 is_finer_than P2 or P2 is_finer_than P1 )
P2 in C by A60, A63;
then A64: P2 is a_partition of X by PARTIT1:def_3;
P1 in C by A60, A62;
then P1 is a_partition of X by PARTIT1:def_3;
hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A30, A60, A62, A63, A64, TAXONOM1:def_1; ::_thesis: verum
end;
now__::_thesis:_h_in_union_C
percases ( Cb <> {} or Cb = {} ) ;
supposeA65: Cb <> {} ; ::_thesis: h in union C
defpred S4[ set ] means $1 misses h;
A66: {h} c= H
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in {h} or s in H )
assume s in {h} ; ::_thesis: s in H
hence s in H by A35, TARSKI:def_1; ::_thesis: verum
end;
consider PX, Pmax being set such that
PX in Cb and
A67: Pmax in Cb and
A68: for PZ being set st PZ in Cb holds
( PZ is_finer_than Pmax & PX is_finer_than PZ ) by A3, A60, A61, A65, XBOOLE_1:1;
consider Pb being set such that
A69: for x being set holds
( x in Pb iff ( x in Pmax & S4[x] ) ) from XBOOLE_0:sch_1();
set PS1 = Pb \/ {h};
set C1 = C \/ {(Pb \/ {h})};
Pmax in C by A60, A67;
then A70: Pmax is a_partition of X by PARTIT1:def_3;
A71: Pmax c= H by A11, A28, A60, A67;
then A72: for a being set holds
( not a in Pmax or a c= h or h c= a or h misses a ) by A10, A35, Def3;
Pb c= Pmax
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in Pb or s in Pmax )
assume s in Pb ; ::_thesis: s in Pmax
hence s in Pmax by A69; ::_thesis: verum
end;
then Pb c= H by A71, XBOOLE_1:1;
then A73: Pb \/ {h} c= H by A66, XBOOLE_1:8;
A74: now__::_thesis:_for_P3_being_set_st_P3_in_C_\/_{(Pb_\/_{h})}_holds_
P3_c=_H
let P3 be set ; ::_thesis: ( P3 in C \/ {(Pb \/ {h})} implies b1 c= H )
assume A75: P3 in C \/ {(Pb \/ {h})} ; ::_thesis: b1 c= H
percases ( P3 in C or P3 in {(Pb \/ {h})} ) by A75, XBOOLE_0:def_3;
suppose P3 in C ; ::_thesis: b1 c= H
hence P3 c= H by A11, A28; ::_thesis: verum
end;
suppose P3 in {(Pb \/ {h})} ; ::_thesis: b1 c= H
hence P3 c= H by A73, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
Pb \/ {h} in {(Pb \/ {h})} by TARSKI:def_1;
then A76: Pb \/ {h} in C \/ {(Pb \/ {h})} by XBOOLE_0:def_3;
h in {h} by TARSKI:def_1;
then A77: h in Pb \/ {h} by XBOOLE_0:def_3;
A78: ex hx being set st
( hx in Pmax & hx c= h & h <> hx ) by A39, A67;
then A79: Pmax is_finer_than Pb \/ {h} by A35, A42, A70, A69, A72, Th19;
A80: now__::_thesis:_for_P3_being_set_holds_
(_not_P3_in_C_or_Pb_\/_{h}_is_finer_than_P3_or_P3_is_finer_than_Pb_\/_{h}_)
let P3 be set ; ::_thesis: ( not P3 in C or Pb \/ {h} is_finer_than b1 or b1 is_finer_than Pb \/ {h} )
assume A81: P3 in C ; ::_thesis: ( Pb \/ {h} is_finer_than b1 or b1 is_finer_than Pb \/ {h} )
percases ( Ca = {} or Ca <> {} ) ;
suppose Ca = {} ; ::_thesis: ( Pb \/ {h} is_finer_than b1 or b1 is_finer_than Pb \/ {h} )
then P3 is_finer_than Pmax by A48, A68, A81;
hence ( Pb \/ {h} is_finer_than P3 or P3 is_finer_than Pb \/ {h} ) by A79, SETFAM_1:17; ::_thesis: verum
end;
supposeA82: Ca <> {} ; ::_thesis: ( Pb \/ {h} is_finer_than b1 or b1 is_finer_than Pb \/ {h} )
now__::_thesis:_(_Pb_\/_{h}_is_finer_than_P3_or_P3_is_finer_than_Pb_\/_{h}_)
percases ( P3 in Ca or P3 in Cb ) by A48, A81, XBOOLE_0:def_3;
supposeA83: P3 in Ca ; ::_thesis: ( Pb \/ {h} is_finer_than P3 or P3 is_finer_than Pb \/ {h} )
consider Pmin, PY being set such that
A84: Pmin in Ca and
PY in Ca and
A85: for PZ being set st PZ in Ca holds
( PZ is_finer_than PY & Pmin is_finer_than PZ ) by A3, A55, A56, A82, XBOOLE_1:1;
A86: Pmin is_finer_than P3 by A83, A85;
A87: now__::_thesis:_not_Pmin_is_finer_than_Pmax
consider hx being set such that
A88: hx in Pmin and
A89: h c= hx and
A90: h <> hx by A37, A84;
assume Pmin is_finer_than Pmax ; ::_thesis: contradiction
then consider hz being set such that
A91: hz in Pmax and
A92: hx c= hz by A88, SETFAM_1:def_2;
consider hy being set such that
A93: hy in Pmax and
A94: hy c= h and
h <> hy by A39, A67;
A95: not hy is empty by A70, A93, EQREL_1:def_4;
hy c= hx by A89, A94, XBOOLE_1:1;
then hy meets hz by A92, A95, Lm4, XBOOLE_1:1;
then hy = hz by A70, A93, A91, EQREL_1:def_4;
then hx c= h by A94, A92, XBOOLE_1:1;
hence contradiction by A89, A90, XBOOLE_0:def_10; ::_thesis: verum
end;
A96: Pmax in C by A54, A67, XBOOLE_0:def_3;
then A97: Pmax is a_partition of X by PARTIT1:def_3;
Pmin in C by A55, A84;
then A98: Pmin is a_partition of X by PARTIT1:def_3;
A99: ex hw being set st
( hw in Pmin & h c= hw & h <> hw ) by A37, A84;
A100: Pmin in C by A54, A84, XBOOLE_0:def_3;
then Pmin is a_partition of X by PARTIT1:def_3;
then Pmax is_finer_than Pmin by A30, A100, A96, A97, A87, TAXONOM1:def_1;
then Pb \/ {h} is_finer_than Pmin by A35, A42, A70, A69, A72, A78, A98, A99, Th19;
hence ( Pb \/ {h} is_finer_than P3 or P3 is_finer_than Pb \/ {h} ) by A86, SETFAM_1:17; ::_thesis: verum
end;
suppose P3 in Cb ; ::_thesis: ( Pb \/ {h} is_finer_than P3 or P3 is_finer_than Pb \/ {h} )
then P3 is_finer_than Pmax by A68;
hence ( Pb \/ {h} is_finer_than P3 or P3 is_finer_than Pb \/ {h} ) by A79, SETFAM_1:17; ::_thesis: verum
end;
end;
end;
hence ( Pb \/ {h} is_finer_than P3 or P3 is_finer_than Pb \/ {h} ) ; ::_thesis: verum
end;
end;
end;
A101: now__::_thesis:_for_P1,_P2_being_set_st_P1_in_C_\/_{(Pb_\/_{h})}_&_P2_in_C_\/_{(Pb_\/_{h})}_&_not_P1_is_finer_than_P2_holds_
P2_is_finer_than_P1
let P1, P2 be set ; ::_thesis: ( P1 in C \/ {(Pb \/ {h})} & P2 in C \/ {(Pb \/ {h})} & not b1 is_finer_than b2 implies b2 is_finer_than b1 )
assume that
A102: P1 in C \/ {(Pb \/ {h})} and
A103: P2 in C \/ {(Pb \/ {h})} ; ::_thesis: ( b1 is_finer_than b2 or b2 is_finer_than b1 )
percases ( P1 in C or P1 in {(Pb \/ {h})} ) by A102, XBOOLE_0:def_3;
supposeA104: P1 in C ; ::_thesis: ( b1 is_finer_than b2 or b2 is_finer_than b1 )
percases ( P2 in C or P2 in {(Pb \/ {h})} ) by A103, XBOOLE_0:def_3;
supposeA105: P2 in C ; ::_thesis: ( b1 is_finer_than b2 or b2 is_finer_than b1 )
then A106: P2 is a_partition of X by PARTIT1:def_3;
P1 is a_partition of X by A104, PARTIT1:def_3;
hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A30, A104, A105, A106, TAXONOM1:def_1; ::_thesis: verum
end;
suppose P2 in {(Pb \/ {h})} ; ::_thesis: ( b1 is_finer_than b2 or b2 is_finer_than b1 )
then P2 = Pb \/ {h} by TARSKI:def_1;
hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A80, A104; ::_thesis: verum
end;
end;
end;
suppose P1 in {(Pb \/ {h})} ; ::_thesis: ( b1 is_finer_than b2 or b2 is_finer_than b1 )
then A107: P1 = Pb \/ {h} by TARSKI:def_1;
percases ( P2 in C or P2 in {(Pb \/ {h})} ) by A103, XBOOLE_0:def_3;
suppose P2 in C ; ::_thesis: ( b1 is_finer_than b2 or b2 is_finer_than b1 )
hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A80, A107; ::_thesis: verum
end;
suppose P2 in {(Pb \/ {h})} ; ::_thesis: ( b1 is_finer_than b2 or b2 is_finer_than b1 )
hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A107, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
end;
end;
A108: Pb \/ {h} is a_partition of X by A35, A42, A70, A69, A72, A78, Th19;
{(Pb \/ {h})} c= PARTITIONS X
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in {(Pb \/ {h})} or s in PARTITIONS X )
assume s in {(Pb \/ {h})} ; ::_thesis: s in PARTITIONS X
then s = Pb \/ {h} by TARSKI:def_1;
hence s in PARTITIONS X by A108, PARTIT1:def_3; ::_thesis: verum
end;
then C \/ {(Pb \/ {h})} c= PARTITIONS X by XBOOLE_1:8;
then C \/ {(Pb \/ {h})} in RL by A11, A74, A101;
then C = C \/ {(Pb \/ {h})} by A29, XBOOLE_1:7;
hence h in union C by A77, A76, TARSKI:def_4; ::_thesis: verum
end;
supposeA109: Cb = {} ; ::_thesis: h in union C
then consider Pmin, PY being set such that
A110: Pmin in Ca and
PY in Ca and
A111: for PZ being set st PZ in Ca holds
( PZ is_finer_than PY & Pmin is_finer_than PZ ) by A3, A33, A54, A56;
consider hw being set such that
A112: hw in Pmin and
A113: h c= hw and
h <> hw by A37, A110;
defpred S4[ set ] means $1 c= hw;
consider PT being set such that
A114: for a being set holds
( a in PT iff ( a in PS & S4[a] ) ) from XBOOLE_0:sch_1();
set PS1 = PT \/ (Pmin \ {hw});
set C1 = C \/ {(PT \/ (Pmin \ {hw}))};
PT c= PS
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in PT or s in PS )
assume s in PT ; ::_thesis: s in PS
hence s in PS by A114; ::_thesis: verum
end;
then A115: PT c= H by A41, XBOOLE_1:1;
A116: Pmin c= H by A11, A28, A55, A110;
then Pmin \ {hw} c= H by XBOOLE_1:1;
then A117: PT \/ (Pmin \ {hw}) c= H by A115, XBOOLE_1:8;
A118: now__::_thesis:_for_P3_being_set_st_P3_in_C_\/_{(PT_\/_(Pmin_\_{hw}))}_holds_
P3_c=_H
let P3 be set ; ::_thesis: ( P3 in C \/ {(PT \/ (Pmin \ {hw}))} implies b1 c= H )
assume A119: P3 in C \/ {(PT \/ (Pmin \ {hw}))} ; ::_thesis: b1 c= H
percases ( P3 in C or P3 in {(PT \/ (Pmin \ {hw}))} ) by A119, XBOOLE_0:def_3;
suppose P3 in C ; ::_thesis: b1 c= H
hence P3 c= H by A11, A28; ::_thesis: verum
end;
suppose P3 in {(PT \/ (Pmin \ {hw}))} ; ::_thesis: b1 c= H
hence P3 c= H by A117, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
Pmin in C by A55, A110;
then A120: Pmin is a_partition of X by PARTIT1:def_3;
A121: for a being set holds
( not a in PS or a c= hw or hw c= a or hw misses a ) by A10, A41, A116, A112, Def3;
then A122: PT \/ (Pmin \ {hw}) is_finer_than Pmin by A40, A42, A120, A112, A113, A114, Th18;
A123: now__::_thesis:_for_P3_being_set_holds_
(_not_P3_in_C_or_PT_\/_(Pmin_\_{hw})_is_finer_than_P3_or_P3_is_finer_than_PT_\/_(Pmin_\_{hw})_)
let P3 be set ; ::_thesis: ( not P3 in C or PT \/ (Pmin \ {hw}) is_finer_than P3 or P3 is_finer_than PT \/ (Pmin \ {hw}) )
assume P3 in C ; ::_thesis: ( PT \/ (Pmin \ {hw}) is_finer_than P3 or P3 is_finer_than PT \/ (Pmin \ {hw}) )
then Pmin is_finer_than P3 by A48, A109, A111;
hence ( PT \/ (Pmin \ {hw}) is_finer_than P3 or P3 is_finer_than PT \/ (Pmin \ {hw}) ) by A122, SETFAM_1:17; ::_thesis: verum
end;
A124: now__::_thesis:_for_P1,_P2_being_set_st_P1_in_C_\/_{(PT_\/_(Pmin_\_{hw}))}_&_P2_in_C_\/_{(PT_\/_(Pmin_\_{hw}))}_&_not_P1_is_finer_than_P2_holds_
P2_is_finer_than_P1
let P1, P2 be set ; ::_thesis: ( P1 in C \/ {(PT \/ (Pmin \ {hw}))} & P2 in C \/ {(PT \/ (Pmin \ {hw}))} & not b1 is_finer_than b2 implies b2 is_finer_than b1 )
assume that
A125: P1 in C \/ {(PT \/ (Pmin \ {hw}))} and
A126: P2 in C \/ {(PT \/ (Pmin \ {hw}))} ; ::_thesis: ( b1 is_finer_than b2 or b2 is_finer_than b1 )
percases ( P1 in C or P1 in {(PT \/ (Pmin \ {hw}))} ) by A125, XBOOLE_0:def_3;
supposeA127: P1 in C ; ::_thesis: ( b1 is_finer_than b2 or b2 is_finer_than b1 )
percases ( P2 in C or P2 in {(PT \/ (Pmin \ {hw}))} ) by A126, XBOOLE_0:def_3;
supposeA128: P2 in C ; ::_thesis: ( b1 is_finer_than b2 or b2 is_finer_than b1 )
then A129: P2 is a_partition of X by PARTIT1:def_3;
P1 is a_partition of X by A127, PARTIT1:def_3;
hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A30, A127, A128, A129, TAXONOM1:def_1; ::_thesis: verum
end;
suppose P2 in {(PT \/ (Pmin \ {hw}))} ; ::_thesis: ( b1 is_finer_than b2 or b2 is_finer_than b1 )
then P2 = PT \/ (Pmin \ {hw}) by TARSKI:def_1;
hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A123, A127; ::_thesis: verum
end;
end;
end;
suppose P1 in {(PT \/ (Pmin \ {hw}))} ; ::_thesis: ( b1 is_finer_than b2 or b2 is_finer_than b1 )
then A130: P1 = PT \/ (Pmin \ {hw}) by TARSKI:def_1;
percases ( P2 in C or P2 in {(PT \/ (Pmin \ {hw}))} ) by A126, XBOOLE_0:def_3;
suppose P2 in C ; ::_thesis: ( b1 is_finer_than b2 or b2 is_finer_than b1 )
hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A123, A130; ::_thesis: verum
end;
suppose P2 in {(PT \/ (Pmin \ {hw}))} ; ::_thesis: ( b1 is_finer_than b2 or b2 is_finer_than b1 )
hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A130, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
end;
end;
A131: PT \/ (Pmin \ {hw}) is a_partition of X by A40, A42, A120, A112, A113, A114, A121, Th18;
{(PT \/ (Pmin \ {hw}))} c= PARTITIONS X
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in {(PT \/ (Pmin \ {hw}))} or s in PARTITIONS X )
assume s in {(PT \/ (Pmin \ {hw}))} ; ::_thesis: s in PARTITIONS X
then s = PT \/ (Pmin \ {hw}) by TARSKI:def_1;
hence s in PARTITIONS X by A131, PARTIT1:def_3; ::_thesis: verum
end;
then C \/ {(PT \/ (Pmin \ {hw}))} c= PARTITIONS X by XBOOLE_1:8;
then C \/ {(PT \/ (Pmin \ {hw}))} in RL by A11, A118, A124;
then A132: C = C \/ {(PT \/ (Pmin \ {hw}))} by A29, XBOOLE_1:7;
A133: PT c= PT \/ (Pmin \ {hw}) by XBOOLE_1:7;
A134: PT \/ (Pmin \ {hw}) in {(PT \/ (Pmin \ {hw}))} by TARSKI:def_1;
A135: {(PT \/ (Pmin \ {hw}))} c= C \/ {(PT \/ (Pmin \ {hw}))} by XBOOLE_1:7;
h in PT by A40, A113, A114;
hence h in union C by A133, A135, A134, A132, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
hence h in union C ; ::_thesis: verum
end;
suppose h in union C ; ::_thesis: h in union C
hence h in union C ; ::_thesis: verum
end;
end;
end;
take C ; ::_thesis: ( C is Classification of X & union C = H )
union C c= H
proof
let h be set ; :: according to TARSKI:def_3 ::_thesis: ( not h in union C or h in H )
assume h in union C ; ::_thesis: h in H
then consider P being set such that
A136: h in P and
A137: P in C by TARSKI:def_4;
P c= H by A11, A28, A137;
hence h in H by A136; ::_thesis: verum
end;
hence ( C is Classification of X & union C = H ) by A30, A34, XBOOLE_0:def_10; ::_thesis: verum
end;