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