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

suppose A3: 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

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

suppose A6: 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 P9 being set such that
A7: for T being set holds
( T in P9 iff ( T in H & S₁[T] ) ) from XFAMILY:sch 1();
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 ) ) )

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

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;