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

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

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

set P' = {} ;
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:54, XBOOLE_1:2; :: thesis: verum

end;

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

now

per cases ( Y in H or not Y in H ) ;

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

set P = {Y};
A5: {Y} is a_partition of Y by A3, EQREL_1:48;
{Y} c= H

proof

let p be set ; :: according to TARSKI:def 3 :: thesis: ( not p in {Y} or p in H )
assume A6: p in {Y} ; :: thesis: p in H
thus p in H by A4, A6, TARSKI:def 1; :: thesis: verum

end;

hence ex P being a_partition of Y st P c= H by A5; :: thesis: verum

end;

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

defpred S₁[ 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 P' being set such that
A8: for T being set holds
( T in P' iff ( T in H & S₁[T] ) ) from XBOOLE_0:sch 1();
A9: union H = Y by ABIAN:4;
A10: P' c= H

proof

let p be set ; :: according to TARSKI:def 3 :: thesis: ( not p in P' or p in H )
assume A11: p in P' ; :: thesis: p in H
thus p in H by A8, A11; :: thesis: verum

end;

then reconsider P = P' as Subset-Family of Y by XBOOLE_1:1;
A12: union P = Y

proof

thus union P c= Y ; :: according to XBOOLE_0:def 10 :: thesis: Y c= union P
thus Y c= union P :: thesis: verum

proof

let p be set ; :: according to TARSKI:def 3 :: thesis: ( not p in Y or p in union P )
assume A13: p in Y ; :: thesis: p in union P
consider h' being set such that
A14: ( p in h' & h' in H ) by A9, A13, TARSKI:def 4;
reconsider h = h' as Subset of Y by A14;
consider T being Subset of Y such that
A15: ( h c= T & T in H & ( for V being Subset of Y st T c= V & V in H holds
V = Y ) ) by A1, A14, Def8;
T in P by A8, A15;
hence p in union P by A14, A15, TARSKI:def 4; :: thesis: verum

end;

end;

now

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

assume A17: S1 = {} ; :: thesis: contradiction
consider S being Subset of Y such that
A18: S in H and
A19: S c= S1 and
A20: for V being Subset of Y st S1 c= V & V in H holds
V = Y by A8, A16;
S1 c= S by A17, XBOOLE_1:2;
then S1 = S by A19, XBOOLE_0:def 10
.= Y by A17, A18, A20, XBOOLE_1:2 ;
hence contradiction by A3, A17; :: 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 A21: S2 in P ; :: thesis: ( S1 = S2 or S1 misses S2 )
A22: S2 in H by A8, A21;
consider T being Subset of Y such that
T in H and
T c= S2 and
A23: for V being Subset of Y st S2 c= V & V in H holds
V = Y by A8, A21;
thus ( S1 = S2 or S1 misses S2 ) by A7, A22, A23; :: thesis: verum

end;

end;

then P is a_partition of Y by A12, EQREL_1:def 6;
hence ex P being a_partition of Y st P c= H by A10; :: thesis: verum

end;

end;

end;

hence ex P being a_partition of Y st P c= H ; :: thesis: verum

end;

end;