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 object 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, Th16;

set L = {PX};

A6: {PX} c= PARTITIONS X

defpred S_{1}[ 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) & S_{1}[L] ) )
from XFAMILY: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;

A26: C in RL and

A27: 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, A26;

A28: C is Classification of X

A32: H c= union C

union C c= H

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 object 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, Th16;

set L = {PX};

A6: {PX} c= PARTITIONS X

proof

let l be object ; :: 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;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

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

A10:
H is hierarchic
by Def4;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;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

defpred S

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) & S

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

then consider C being set such that 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: for X1, X2 being set st X1 in Z & X2 in Z & not X1 c= X2 holds

X2 c= X1 by XBOOLE_0:def 9, A14, ORDINAL1:def 8;

X1 c= Y ) )

X1 c= Y

thus for X1 being set st X1 in Z holds

X1 c= Y by ZFMISC_1:74; :: thesis: verum

end;( 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: for X1, X2 being set st X1 in Z & X2 in Z & not X1 c= X2 holds

X2 c= X1 by XBOOLE_0:def 9, A14, ORDINAL1:def 8;

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

take Y = union Z; :: thesis: ( Y in RL & ( for X1 being set st X1 in Z holds P2 is_finer_than P1

let P1, P2 be set ; :: thesis: ( P1 in union Z & P2 in union Z & not b_{1} is_finer_than b_{2} implies b_{2} is_finer_than b_{1} )

assume that

A17: P1 in union Z and

A18: P2 in union Z ; :: thesis: ( b_{1} is_finer_than b_{2} or b_{2} is_finer_than b_{1} )

consider L1 being set such that

A19: P1 in L1 and

A20: L1 in Z by A17, TARSKI:def 4;

consider L2 being set such that

A21: P2 in L2 and

A22: L2 in Z by A18, TARSKI:def 4;

end;assume that

A17: P1 in union Z and

A18: P2 in union Z ; :: thesis: ( b

consider L1 being set such that

A19: P1 in L1 and

A20: L1 in Z by A17, TARSKI:def 4;

consider L2 being set such that

A21: P2 in L2 and

A22: L2 in Z by A18, TARSKI:def 4;

per cases
( L1 c= L2 or L2 c= L1 )
by A15, A20, A22;

end;

X1 c= Y ) )

A23: now :: thesis: for P being set st P in Y holds

P c= H

Y c= PARTITIONS X
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;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

proof

hence
Y in RL
by A11, A23, A16; :: thesis: for X1 being set st X1 in Z holds
let P be object ; :: 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

A24: P in L4 and

A25: L4 in Z by TARSKI:def 4;

L4 in bool (PARTITIONS X) by A11, A13, A25;

hence P in PARTITIONS X by A24; :: thesis: verum

end;assume P in Y ; :: thesis: P in PARTITIONS X

then consider L4 being set such that

A24: P in L4 and

A25: L4 in Z by TARSKI:def 4;

L4 in bool (PARTITIONS X) by A11, A13, A25;

hence P in PARTITIONS X by A24; :: thesis: verum

X1 c= Y

thus for X1 being set st X1 in Z holds

X1 c= Y by ZFMISC_1:74; :: thesis: verum

A26: C in RL and

A27: 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, A26;

A28: C is Classification of X

proof

A31:
C <> {}
by A12, A27, XBOOLE_1:2;
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

A29: P1 in C and

A30: 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, A26, A29, A30; :: thesis: verum

end;assume that

A29: P1 in C and

A30: 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, A26, A29, A30; :: thesis: verum

A32: H c= union C

proof

take
C
; :: thesis: ( C is Classification of X & union C = H )
let h be object ; :: according to TARSKI:def 3 :: thesis: ( not h in H or h in union C )

assume A33: h in H ; :: thesis: h in union C

reconsider hh = h as set by TARSKI:1;

end;assume A33: h in H ; :: thesis: h in union C

reconsider hh = h as set by TARSKI:1;

per cases
( not h in union C or h in union C )
;

end;

suppose A34:
not h in union C
; :: thesis: h in union C

defpred S_{2}[ set ] means ex hx being set st

( hx in $1 & hh c= hx & h <> hx );

consider Ca being set such that

A35: for p being set holds

( p in Ca iff ( p in C & S_{2}[p] ) )
from XFAMILY:sch 1();

A36: Ca c= C by A35;

defpred S_{3}[ set ] means ex hx being set st

( hx in $1 & hx c= hh & h <> hx );

consider Cb being set such that

A37: for p being set holds

( p in Cb iff ( p in C & S_{3}[p] ) )
from XFAMILY:sch 1();

consider PS being a_partition of X such that

A38: h in PS and

A39: PS c= H by A1, A2, A33, Th16;

A40: h <> {} by A38, EQREL_1:def 4;

then Ca \/ Cb c= C by A36, XBOOLE_1:8;

then A52: C = Ca \/ Cb by A46, XBOOLE_0:def 10;

then A53: Ca c= C by XBOOLE_1:7;

end;( hx in $1 & hh c= hx & h <> hx );

consider Ca being set such that

A35: for p being set holds

( p in Ca iff ( p in C & S

A36: Ca c= C by A35;

defpred S

( hx in $1 & hx c= hh & h <> hx );

consider Cb being set such that

A37: for p being set holds

( p in Cb iff ( p in C & S

consider PS being a_partition of X such that

A38: h in PS and

A39: PS c= H by A1, A2, A33, Th16;

A40: h <> {} by A38, EQREL_1:def 4;

A41: now :: thesis: for p being set st p in C holds

ex hv being set st

( hv in p & not hv misses hh )

A46:
C c= Ca \/ Cb
ex hv being set st

( hv in p & not hv misses hh )

consider t being object such that

A42: t in hh by A40, XBOOLE_0:def 1;

let p be set ; :: thesis: ( p in C implies ex hv being set st

( hv in p & not hv misses hh ) )

assume p in C ; :: thesis: ex hv being set st

( hv in p & not hv misses hh )

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

A43: t in v and

A44: v in p by A33, A42, TARSKI:def 4;

assume A45: for hv being set st hv in p holds

hv misses hh ; :: thesis: contradiction

not v misses hh by A42, A43, XBOOLE_0:3;

hence contradiction by A45, A44; :: thesis: verum

end;A42: t in hh by A40, XBOOLE_0:def 1;

let p be set ; :: thesis: ( p in C implies ex hv being set st

( hv in p & not hv misses hh ) )

assume p in C ; :: thesis: ex hv being set st

( hv in p & not hv misses hh )

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

A43: t in v and

A44: v in p by A33, A42, TARSKI:def 4;

assume A45: for hv being set st hv in p holds

hv misses hh ; :: thesis: contradiction

not v misses hh by A42, A43, XBOOLE_0:3;

hence contradiction by A45, A44; :: thesis: verum

proof

Cb c= C
by A37;
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in C or p in Ca \/ Cb )

assume A47: p in C ; :: thesis: p in Ca \/ Cb

reconsider pp = p as set by TARSKI:1;

consider hv being set such that

A48: hv in pp and

A49: not hv misses hh by A41, A47;

A50: h <> hv by A34, A47, A48, TARSKI:def 4;

A51: pp c= H by A11, A26, A47;

end;assume A47: p in C ; :: thesis: p in Ca \/ Cb

reconsider pp = p as set by TARSKI:1;

consider hv being set such that

A48: hv in pp and

A49: not hv misses hh by A41, A47;

A50: h <> hv by A34, A47, A48, TARSKI:def 4;

A51: pp c= H by A11, A26, A47;

then Ca \/ Cb c= C by A36, XBOOLE_1:8;

then A52: C = Ca \/ Cb by A46, XBOOLE_0:def 10;

then A53: Ca c= C by XBOOLE_1:7;

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

A58:
Cb c= C
by A52, XBOOLE_1:7;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

A55: P1 in Ca and

A56: P2 in Ca ; :: thesis: ( P1 is_finer_than P2 or P2 is_finer_than P1 )

P2 in C by A53, A56;

then A57: P2 is a_partition of X by PARTIT1:def 3;

P1 in C by A53, A55;

then P1 is a_partition of X by PARTIT1:def 3;

hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A28, A53, A55, A56, A57, TAXONOM1:def 1; :: thesis: verum

end;assume that

A55: P1 in Ca and

A56: P2 in Ca ; :: thesis: ( P1 is_finer_than P2 or P2 is_finer_than P1 )

P2 in C by A53, A56;

then A57: P2 is a_partition of X by PARTIT1:def 3;

P1 in C by A53, A55;

then P1 is a_partition of X by PARTIT1:def 3;

hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A28, A53, A55, A56, A57, TAXONOM1:def 1; :: thesis: verum

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

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

A60: P1 in Cb and

A61: P2 in Cb ; :: thesis: ( P1 is_finer_than P2 or P2 is_finer_than P1 )

P2 in C by A58, A61;

then A62: P2 is a_partition of X by PARTIT1:def 3;

P1 in C by A58, A60;

then P1 is a_partition of X by PARTIT1:def 3;

hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A28, A58, A60, A61, A62, TAXONOM1:def 1; :: thesis: verum

end;assume that

A60: P1 in Cb and

A61: P2 in Cb ; :: thesis: ( P1 is_finer_than P2 or P2 is_finer_than P1 )

P2 in C by A58, A61;

then A62: P2 is a_partition of X by PARTIT1:def 3;

P1 in C by A58, A60;

then P1 is a_partition of X by PARTIT1:def 3;

hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A28, A58, A60, A61, A62, TAXONOM1:def 1; :: thesis: verum

now :: thesis: h in union Cend;

hence
h in union C
; :: thesis: verumper cases
( Cb <> {} or Cb = {} )
;

end;

suppose A63:
Cb <> {}
; :: thesis: h in union C

defpred S_{4}[ set ] means $1 misses hh;

A64: {h} c= H by A33, TARSKI:def 1;

consider PX, Pmax being set such that

PX in Cb and

A65: Pmax in Cb and

A66: for PZ being set st PZ in Cb holds

( PZ is_finer_than Pmax & PX is_finer_than PZ ) by A3, A58, A59, A63, XBOOLE_1:1;

consider Pb being set such that

A67: for x being set holds

( x in Pb iff ( x in Pmax & S_{4}[x] ) )
from XFAMILY:sch 1();

set PS1 = Pb \/ {h};

set C1 = C \/ {(Pb \/ {h})};

Pmax in C by A58, A65;

then A68: Pmax is a_partition of X by PARTIT1:def 3;

A69: Pmax c= H by A11, A26, A58, A65;

then A70: for a being set holds

( not a in Pmax or a c= hh or hh c= a or hh misses a ) by A10, A33;

Pb c= Pmax by A67;

then Pb c= H by A69;

then A71: Pb \/ {h} c= H by A64, XBOOLE_1:8;

then A74: Pb \/ {h} in C \/ {(Pb \/ {h})} by XBOOLE_0:def 3;

h in {h} by TARSKI:def 1;

then A75: h in Pb \/ {h} by XBOOLE_0:def 3;

A76: ex hx being set st

( hx in Pmax & hx c= hh & hh <> hx ) by A37, A65;

then A77: Pmax is_finer_than Pb \/ {h} by A33, A40, A68, A67, A70, Th18;

{(Pb \/ {h})} c= PARTITIONS X

then C \/ {(Pb \/ {h})} in RL by A11, A72, A99;

then C = C \/ {(Pb \/ {h})} by A27, XBOOLE_1:7;

hence h in union C by A75, A74, TARSKI:def 4; :: thesis: verum

end;A64: {h} c= H by A33, TARSKI:def 1;

consider PX, Pmax being set such that

PX in Cb and

A65: Pmax in Cb and

A66: for PZ being set st PZ in Cb holds

( PZ is_finer_than Pmax & PX is_finer_than PZ ) by A3, A58, A59, A63, XBOOLE_1:1;

consider Pb being set such that

A67: for x being set holds

( x in Pb iff ( x in Pmax & S

set PS1 = Pb \/ {h};

set C1 = C \/ {(Pb \/ {h})};

Pmax in C by A58, A65;

then A68: Pmax is a_partition of X by PARTIT1:def 3;

A69: Pmax c= H by A11, A26, A58, A65;

then A70: for a being set holds

( not a in Pmax or a c= hh or hh c= a or hh misses a ) by A10, A33;

Pb c= Pmax by A67;

then Pb c= H by A69;

then A71: Pb \/ {h} c= H by A64, XBOOLE_1:8;

A72: now :: thesis: for P3 being set st P3 in C \/ {(Pb \/ {h})} holds

P3 c= H

Pb \/ {h} in {(Pb \/ {h})}
by TARSKI:def 1;P3 c= H

let P3 be set ; :: thesis: ( P3 in C \/ {(Pb \/ {h})} implies b_{1} c= H )

assume A73: P3 in C \/ {(Pb \/ {h})} ; :: thesis: b_{1} c= H

end;assume A73: P3 in C \/ {(Pb \/ {h})} ; :: thesis: b

then A74: Pb \/ {h} in C \/ {(Pb \/ {h})} by XBOOLE_0:def 3;

h in {h} by TARSKI:def 1;

then A75: h in Pb \/ {h} by XBOOLE_0:def 3;

A76: ex hx being set st

( hx in Pmax & hx c= hh & hh <> hx ) by A37, A65;

then A77: Pmax is_finer_than Pb \/ {h} by A33, A40, A68, A67, A70, Th18;

A78: 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} )

( 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 b_{1} or b_{1} is_finer_than Pb \/ {h} )

assume A79: P3 in C ; :: thesis: ( Pb \/ {h} is_finer_than b_{1} or b_{1} is_finer_than Pb \/ {h} )

end;assume A79: P3 in C ; :: thesis: ( Pb \/ {h} is_finer_than b

per cases
( Ca = {} or Ca <> {} )
;

end;

suppose
Ca = {}
; :: thesis: ( Pb \/ {h} is_finer_than b_{1} or b_{1} is_finer_than Pb \/ {h} )

then
P3 is_finer_than Pmax
by A46, A66, A79;

hence ( Pb \/ {h} is_finer_than P3 or P3 is_finer_than Pb \/ {h} ) by A77, SETFAM_1:17; :: thesis: verum

end;hence ( Pb \/ {h} is_finer_than P3 or P3 is_finer_than Pb \/ {h} ) by A77, SETFAM_1:17; :: thesis: verum

suppose A80:
Ca <> {}
; :: thesis: ( Pb \/ {h} is_finer_than b_{1} or b_{1} is_finer_than Pb \/ {h} )

end;

now :: thesis: ( Pb \/ {h} is_finer_than P3 or P3 is_finer_than Pb \/ {h} )end;

hence
( Pb \/ {h} is_finer_than P3 or P3 is_finer_than Pb \/ {h} )
; :: thesis: verumper cases
( P3 in Ca or P3 in Cb )
by A46, A79, XBOOLE_0:def 3;

end;

suppose A81:
P3 in Ca
; :: thesis: ( Pb \/ {h} is_finer_than P3 or P3 is_finer_than Pb \/ {h} )

consider Pmin, PY being set such that

A82: Pmin in Ca and

PY in Ca and

A83: for PZ being set st PZ in Ca holds

( PZ is_finer_than PY & Pmin is_finer_than PZ ) by A3, A53, A54, A80, XBOOLE_1:1;

A84: Pmin is_finer_than P3 by A81, A83;

then A95: Pmax is a_partition of X by PARTIT1:def 3;

Pmin in C by A53, A82;

then A96: Pmin is a_partition of X by PARTIT1:def 3;

A97: ex hw being set st

( hw in Pmin & hh c= hw & h <> hw ) by A35, A82;

A98: Pmin in C by A52, A82, XBOOLE_0:def 3;

then Pmin is a_partition of X by PARTIT1:def 3;

then Pmax is_finer_than Pmin by A28, A98, A94, A95, A85, TAXONOM1:def 1;

then Pb \/ {h} is_finer_than Pmin by A33, A40, A68, A67, A70, A76, A96, A97, Th18;

hence ( Pb \/ {h} is_finer_than P3 or P3 is_finer_than Pb \/ {h} ) by A84, SETFAM_1:17; :: thesis: verum

end;A82: Pmin in Ca and

PY in Ca and

A83: for PZ being set st PZ in Ca holds

( PZ is_finer_than PY & Pmin is_finer_than PZ ) by A3, A53, A54, A80, XBOOLE_1:1;

A84: Pmin is_finer_than P3 by A81, A83;

A85: now :: thesis: not Pmin is_finer_than Pmax

A94:
Pmax in C
by A52, A65, XBOOLE_0:def 3;consider hx being set such that

A86: hx in Pmin and

A87: hh c= hx and

A88: h <> hx by A35, A82;

assume Pmin is_finer_than Pmax ; :: thesis: contradiction

then consider hz being set such that

A89: hz in Pmax and

A90: hx c= hz by A86;

consider hy being set such that

A91: hy in Pmax and

A92: hy c= hh and

h <> hy by A37, A65;

A93: not hy is empty by A68, A91, EQREL_1:def 4;

hy c= hx by A87, A92;

then hy meets hz by A90, A93, Lm5, XBOOLE_1:1;

then hy = hz by A68, A91, A89, EQREL_1:def 4;

then hx c= hh by A92, A90;

hence contradiction by A87, A88, XBOOLE_0:def 10; :: thesis: verum

end;A86: hx in Pmin and

A87: hh c= hx and

A88: h <> hx by A35, A82;

assume Pmin is_finer_than Pmax ; :: thesis: contradiction

then consider hz being set such that

A89: hz in Pmax and

A90: hx c= hz by A86;

consider hy being set such that

A91: hy in Pmax and

A92: hy c= hh and

h <> hy by A37, A65;

A93: not hy is empty by A68, A91, EQREL_1:def 4;

hy c= hx by A87, A92;

then hy meets hz by A90, A93, Lm5, XBOOLE_1:1;

then hy = hz by A68, A91, A89, EQREL_1:def 4;

then hx c= hh by A92, A90;

hence contradiction by A87, A88, XBOOLE_0:def 10; :: thesis: verum

then A95: Pmax is a_partition of X by PARTIT1:def 3;

Pmin in C by A53, A82;

then A96: Pmin is a_partition of X by PARTIT1:def 3;

A97: ex hw being set st

( hw in Pmin & hh c= hw & h <> hw ) by A35, A82;

A98: Pmin in C by A52, A82, XBOOLE_0:def 3;

then Pmin is a_partition of X by PARTIT1:def 3;

then Pmax is_finer_than Pmin by A28, A98, A94, A95, A85, TAXONOM1:def 1;

then Pb \/ {h} is_finer_than Pmin by A33, A40, A68, A67, A70, A76, A96, A97, Th18;

hence ( Pb \/ {h} is_finer_than P3 or P3 is_finer_than Pb \/ {h} ) by A84, SETFAM_1:17; :: thesis: verum

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

hence ( Pb \/ {h} is_finer_than P3 or P3 is_finer_than Pb \/ {h} ) by A77, SETFAM_1:17; :: thesis: verum

end;hence ( Pb \/ {h} is_finer_than P3 or P3 is_finer_than Pb \/ {h} ) by A77, SETFAM_1:17; :: thesis: verum

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

A106:
Pb \/ {h} is a_partition of X
by A33, A40, A68, A67, A70, A76, Th18;P2 is_finer_than P1

let P1, P2 be set ; :: thesis: ( P1 in C \/ {(Pb \/ {h})} & P2 in C \/ {(Pb \/ {h})} & not b_{1} is_finer_than b_{2} implies b_{2} is_finer_than b_{1} )

assume that

A100: P1 in C \/ {(Pb \/ {h})} and

A101: P2 in C \/ {(Pb \/ {h})} ; :: thesis: ( b_{1} is_finer_than b_{2} or b_{2} is_finer_than b_{1} )

end;assume that

A100: P1 in C \/ {(Pb \/ {h})} and

A101: P2 in C \/ {(Pb \/ {h})} ; :: thesis: ( b

per cases
( P1 in C or P1 in {(Pb \/ {h})} )
by A100, XBOOLE_0:def 3;

end;

suppose A102:
P1 in C
; :: thesis: ( b_{1} is_finer_than b_{2} or b_{2} is_finer_than b_{1} )

end;

per cases
( P2 in C or P2 in {(Pb \/ {h})} )
by A101, XBOOLE_0:def 3;

end;

suppose A103:
P2 in C
; :: thesis: ( b_{1} is_finer_than b_{2} or b_{2} is_finer_than b_{1} )

then A104:
P2 is a_partition of X
by PARTIT1:def 3;

P1 is a_partition of X by A102, PARTIT1:def 3;

hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A28, A102, A103, A104, TAXONOM1:def 1; :: thesis: verum

end;P1 is a_partition of X by A102, PARTIT1:def 3;

hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A28, A102, A103, A104, TAXONOM1:def 1; :: thesis: verum

suppose
P2 in {(Pb \/ {h})}
; :: thesis: ( b_{1} is_finer_than b_{2} or b_{2} is_finer_than b_{1} )

then
P2 = Pb \/ {h}
by TARSKI:def 1;

hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A78, A102; :: thesis: verum

end;hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A78, A102; :: thesis: verum

suppose
P1 in {(Pb \/ {h})}
; :: thesis: ( b_{1} is_finer_than b_{2} or b_{2} is_finer_than b_{1} )

then A105:
P1 = Pb \/ {h}
by TARSKI:def 1;

end;per cases
( P2 in C or P2 in {(Pb \/ {h})} )
by A101, XBOOLE_0:def 3;

end;

suppose
P2 in {(Pb \/ {h})}
; :: thesis: ( b_{1} is_finer_than b_{2} or b_{2} is_finer_than b_{1} )

end;

end;

{(Pb \/ {h})} c= PARTITIONS X

proof

then
C \/ {(Pb \/ {h})} c= PARTITIONS X
by XBOOLE_1:8;
let s be object ; :: 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 A106, PARTIT1:def 3; :: thesis: verum

end;assume s in {(Pb \/ {h})} ; :: thesis: s in PARTITIONS X

then s = Pb \/ {h} by TARSKI:def 1;

hence s in PARTITIONS X by A106, PARTIT1:def 3; :: thesis: verum

then C \/ {(Pb \/ {h})} in RL by A11, A72, A99;

then C = C \/ {(Pb \/ {h})} by A27, XBOOLE_1:7;

hence h in union C by A75, A74, TARSKI:def 4; :: thesis: verum

suppose A107:
Cb = {}
; :: thesis: h in union C

then consider Pmin, PY being set such that

A108: Pmin in Ca and

PY in Ca and

A109: for PZ being set st PZ in Ca holds

( PZ is_finer_than PY & Pmin is_finer_than PZ ) by A3, A31, A52, A54;

consider hw being set such that

A110: hw in Pmin and

A111: hh c= hw and

hh <> hw by A35, A108;

defpred S_{4}[ set ] means $1 c= hw;

consider PT being set such that

A112: for a being set holds

( a in PT iff ( a in PS & S_{4}[a] ) )
from XFAMILY:sch 1();

set PS1 = PT \/ (Pmin \ {hw});

set C1 = C \/ {(PT \/ (Pmin \ {hw}))};

PT c= PS by A112;

then A113: PT c= H by A39;

A114: Pmin c= H by A11, A26, A53, A108;

then Pmin \ {hw} c= H ;

then A115: PT \/ (Pmin \ {hw}) c= H by A113, XBOOLE_1:8;

then A118: Pmin is a_partition of X by PARTIT1:def 3;

A119: for a being set holds

( not a in PS or a c= hw or hw c= a or hw misses a ) by A10, A39, A114, A110;

then A120: PT \/ (Pmin \ {hw}) is_finer_than Pmin by A38, A40, A118, A110, A111, A112, Th17;

{(PT \/ (Pmin \ {hw}))} c= PARTITIONS X

then C \/ {(PT \/ (Pmin \ {hw}))} in RL by A11, A116, A122;

then A130: C = C \/ {(PT \/ (Pmin \ {hw}))} by A27, XBOOLE_1:7;

A131: PT c= PT \/ (Pmin \ {hw}) by XBOOLE_1:7;

A132: PT \/ (Pmin \ {hw}) in {(PT \/ (Pmin \ {hw}))} by TARSKI:def 1;

A133: {(PT \/ (Pmin \ {hw}))} c= C \/ {(PT \/ (Pmin \ {hw}))} by XBOOLE_1:7;

h in PT by A38, A111, A112;

hence h in union C by A131, A133, A132, A130, TARSKI:def 4; :: thesis: verum

end;A108: Pmin in Ca and

PY in Ca and

A109: for PZ being set st PZ in Ca holds

( PZ is_finer_than PY & Pmin is_finer_than PZ ) by A3, A31, A52, A54;

consider hw being set such that

A110: hw in Pmin and

A111: hh c= hw and

hh <> hw by A35, A108;

defpred S

consider PT being set such that

A112: for a being set holds

( a in PT iff ( a in PS & S

set PS1 = PT \/ (Pmin \ {hw});

set C1 = C \/ {(PT \/ (Pmin \ {hw}))};

PT c= PS by A112;

then A113: PT c= H by A39;

A114: Pmin c= H by A11, A26, A53, A108;

then Pmin \ {hw} c= H ;

then A115: PT \/ (Pmin \ {hw}) c= H by A113, XBOOLE_1:8;

A116: now :: thesis: for P3 being set st P3 in C \/ {(PT \/ (Pmin \ {hw}))} holds

P3 c= H

Pmin in C
by A53, A108;P3 c= H

let P3 be set ; :: thesis: ( P3 in C \/ {(PT \/ (Pmin \ {hw}))} implies b_{1} c= H )

assume A117: P3 in C \/ {(PT \/ (Pmin \ {hw}))} ; :: thesis: b_{1} c= H

end;assume A117: P3 in C \/ {(PT \/ (Pmin \ {hw}))} ; :: thesis: b

then A118: Pmin is a_partition of X by PARTIT1:def 3;

A119: for a being set holds

( not a in PS or a c= hw or hw c= a or hw misses a ) by A10, A39, A114, A110;

then A120: PT \/ (Pmin \ {hw}) is_finer_than Pmin by A38, A40, A118, A110, A111, A112, Th17;

A121: 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}) )

( 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 A46, A107, A109;

hence ( PT \/ (Pmin \ {hw}) is_finer_than P3 or P3 is_finer_than PT \/ (Pmin \ {hw}) ) by A120, SETFAM_1:17; :: thesis: verum

end;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 A46, A107, A109;

hence ( PT \/ (Pmin \ {hw}) is_finer_than P3 or P3 is_finer_than PT \/ (Pmin \ {hw}) ) by A120, SETFAM_1:17; :: thesis: verum

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

A129:
PT \/ (Pmin \ {hw}) is a_partition of X
by A38, A40, A118, A110, A111, A112, A119, Th17;P2 is_finer_than P1

let P1, P2 be set ; :: thesis: ( P1 in C \/ {(PT \/ (Pmin \ {hw}))} & P2 in C \/ {(PT \/ (Pmin \ {hw}))} & not b_{1} is_finer_than b_{2} implies b_{2} is_finer_than b_{1} )

assume that

A123: P1 in C \/ {(PT \/ (Pmin \ {hw}))} and

A124: P2 in C \/ {(PT \/ (Pmin \ {hw}))} ; :: thesis: ( b_{1} is_finer_than b_{2} or b_{2} is_finer_than b_{1} )

end;assume that

A123: P1 in C \/ {(PT \/ (Pmin \ {hw}))} and

A124: P2 in C \/ {(PT \/ (Pmin \ {hw}))} ; :: thesis: ( b

per cases
( P1 in C or P1 in {(PT \/ (Pmin \ {hw}))} )
by A123, XBOOLE_0:def 3;

end;

suppose A125:
P1 in C
; :: thesis: ( b_{1} is_finer_than b_{2} or b_{2} is_finer_than b_{1} )

end;

per cases
( P2 in C or P2 in {(PT \/ (Pmin \ {hw}))} )
by A124, XBOOLE_0:def 3;

end;

suppose A126:
P2 in C
; :: thesis: ( b_{1} is_finer_than b_{2} or b_{2} is_finer_than b_{1} )

then A127:
P2 is a_partition of X
by PARTIT1:def 3;

P1 is a_partition of X by A125, PARTIT1:def 3;

hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A28, A125, A126, A127, TAXONOM1:def 1; :: thesis: verum

end;P1 is a_partition of X by A125, PARTIT1:def 3;

hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A28, A125, A126, A127, TAXONOM1:def 1; :: thesis: verum

suppose
P2 in {(PT \/ (Pmin \ {hw}))}
; :: thesis: ( b_{1} is_finer_than b_{2} or b_{2} is_finer_than b_{1} )

then
P2 = PT \/ (Pmin \ {hw})
by TARSKI:def 1;

hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A121, A125; :: thesis: verum

end;hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A121, A125; :: thesis: verum

suppose
P1 in {(PT \/ (Pmin \ {hw}))}
; :: thesis: ( b_{1} is_finer_than b_{2} or b_{2} is_finer_than b_{1} )

then A128:
P1 = PT \/ (Pmin \ {hw})
by TARSKI:def 1;

end;per cases
( P2 in C or P2 in {(PT \/ (Pmin \ {hw}))} )
by A124, XBOOLE_0:def 3;

end;

suppose
P2 in {(PT \/ (Pmin \ {hw}))}
; :: thesis: ( b_{1} is_finer_than b_{2} or b_{2} is_finer_than b_{1} )

end;

end;

{(PT \/ (Pmin \ {hw}))} c= PARTITIONS X

proof

then
C \/ {(PT \/ (Pmin \ {hw}))} c= PARTITIONS X
by XBOOLE_1:8;
let s be object ; :: 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 A129, PARTIT1:def 3; :: thesis: verum

end;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 A129, PARTIT1:def 3; :: thesis: verum

then C \/ {(PT \/ (Pmin \ {hw}))} in RL by A11, A116, A122;

then A130: C = C \/ {(PT \/ (Pmin \ {hw}))} by A27, XBOOLE_1:7;

A131: PT c= PT \/ (Pmin \ {hw}) by XBOOLE_1:7;

A132: PT \/ (Pmin \ {hw}) in {(PT \/ (Pmin \ {hw}))} by TARSKI:def 1;

A133: {(PT \/ (Pmin \ {hw}))} c= C \/ {(PT \/ (Pmin \ {hw}))} by XBOOLE_1:7;

h in PT by A38, A111, A112;

hence h in union C by A131, A133, A132, A130, TARSKI:def 4; :: thesis: verum

union C c= H

proof

hence
( C is Classification of X & union C = H )
by A28, A32, XBOOLE_0:def 10; :: thesis: verum
let h be object ; :: 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

A134: h in P and

A135: P in C by TARSKI:def 4;

P c= H by A11, A26, A135;

hence h in H by A134; :: thesis: verum

end;assume h in union C ; :: thesis: h in H

then consider P being set such that

A134: h in P and

A135: P in C by TARSKI:def 4;

P c= H by A11, A26, A135;

hence h in H by A134; :: thesis: verum