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 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} 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:48;
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 S1[ set ] means ex S being Subset of st
( S in H & S c= $1 & ( for V being Subset of st $1 c= V & V in H holds
V = Y ) );
consider P' being set such that
A7: for T being set holds
( T in P' iff ( T in H & S1[T] ) ) from XBOOLE_0:sch 1();
A8: P' c= H
proof
let p be set ; :: according to TARSKI:def 3 :: thesis: ( not p in P' or p in H )
assume p in P' ; :: thesis: p in H
hence p in H by A7; :: thesis: verum
end;
then reconsider P = P' as Subset-Family of by XBOOLE_1:1;
A9: now
let S1 be Subset of ; :: thesis: ( S1 in P implies ( S1 <> {} & ( for S2 being Subset of holds
( not S2 in P or S1 = S2 or S1 misses S2 ) ) ) )
assume A10: S1 in P ; :: thesis: ( S1 <> {} & ( for S2 being Subset of holds
( not S2 in P or S1 = S2 or S1 misses S2 ) ) )
thus S1 <> {} :: thesis: for S2 being Subset of holds
( not S2 in P or S1 = S2 or S1 misses S2 )
proof
consider S being Subset of such that
A11: S in H and
A12: S c= S1 and
A13: for V being Subset of 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 holds
( not S2 in P or S1 = S2 or S1 misses S2 ) :: thesis: verum
proof
let S2 be Subset of ; :: 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 st
( T in H & T c= S2 & ( for V being Subset of 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 h' being set such that
A18: p in h' and
A19: h' in H by A17, TARSKI:def 4;
reconsider h = h' as Subset of by A19;
consider T being Subset of such that
A20: h c= T and
A21: T in H and
A22: for V being Subset of 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 6;
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;