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

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

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

end;

suppose A2:
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; :: thesis: verum

end;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; :: thesis: verum

suppose A3:
Y <> {}
; :: thesis: ex P being a_partition of Y st P c= H

end;

now :: thesis: ex P being a_partition of Y st P c= Hend;

hence
ex P being a_partition of Y st P c= H
; :: thesis: verumper cases
( Y in H or not Y in H )
;

end;

suppose A4:
Y in H
; :: thesis: ex P being a_partition of Y st P c= H

set P = {Y};

A5: {Y} c= H by A4, TARSKI:def 1;

{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;A5: {Y} c= H by A4, TARSKI:def 1;

{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

suppose A6:
not Y in H
; :: thesis: ex P being a_partition of Y st P c= H

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

A8: P9 c= H by A7;

then reconsider P = P9 as Subset-Family of Y by XBOOLE_1:1;

Y c= union P

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;( 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 & S

A8: P9 c= H by A7;

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

A17:
union H = Y
by ABIAN:4;( 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 )

( not S2 in P or S1 = S2 or S1 misses S2 ) :: thesis: verum

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

thus
for S2 being Subset of Y holds
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;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

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

Y c= union P

proof

then
union P = Y
by XBOOLE_0:def 10;
let p be object ; :: 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;

T in P by A7, A21, A22;

hence p in union P by A18, A20, TARSKI:def 4; :: thesis: verum

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

T in P by A7, A21, A22;

hence p in union P by A18, A20, TARSKI:def 4; :: thesis: verum

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