let X, h be non empty set ; :: thesis: ( h c= X implies for Pmax being a_partition of X st ex hy being set st
( hy in Pmax & hy c= h ) & ( for x being set holds
( not x in Pmax or x c= h or h c= x or h misses x ) ) holds
for Pb being set st ( for x being set holds
( x in Pb iff ( x in Pmax & x misses h ) ) ) holds
( Pb \/ {h} is a_partition of X & Pmax is_finer_than Pb \/ {h} & ( for Pmin being a_partition of X st Pmax is_finer_than Pmin holds
for hw being set st hw in Pmin & h c= hw holds
Pb \/ {h} is_finer_than Pmin ) ) )

assume A1: h c= X ; :: thesis: for Pmax being a_partition of X st ex hy being set st
( hy in Pmax & hy c= h ) & ( for x being set holds
( not x in Pmax or x c= h or h c= x or h misses x ) ) holds
for Pb being set st ( for x being set holds
( x in Pb iff ( x in Pmax & x misses h ) ) ) holds
( Pb \/ {h} is a_partition of X & Pmax is_finer_than Pb \/ {h} & ( for Pmin being a_partition of X st Pmax is_finer_than Pmin holds
for hw being set st hw in Pmin & h c= hw holds
Pb \/ {h} is_finer_than Pmin ) )

A2: {h} c= bool X
proof
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in {h} or s in bool X )
assume s in {h} ; :: thesis: s in bool X
then s = h by TARSKI:def 1;
hence s in bool X by A1; :: thesis: verum
end;
A3: h in {h} by TARSKI:def 1;
let Pmax be a_partition of X; :: thesis: ( ex hy being set st
( hy in Pmax & hy c= h ) & ( for x being set holds
( not x in Pmax or x c= h or h c= x or h misses x ) ) implies for Pb being set st ( for x being set holds
( x in Pb iff ( x in Pmax & x misses h ) ) ) holds
( Pb \/ {h} is a_partition of X & Pmax is_finer_than Pb \/ {h} & ( for Pmin being a_partition of X st Pmax is_finer_than Pmin holds
for hw being set st hw in Pmin & h c= hw holds
Pb \/ {h} is_finer_than Pmin ) ) )

assume that
A4: ex hy being set st
( hy in Pmax & hy c= h ) and
A5: for x being set holds
( not x in Pmax or x c= h or h c= x or h misses x ) ; :: thesis: for Pb being set st ( for x being set holds
( x in Pb iff ( x in Pmax & x misses h ) ) ) holds
( Pb \/ {h} is a_partition of X & Pmax is_finer_than Pb \/ {h} & ( for Pmin being a_partition of X st Pmax is_finer_than Pmin holds
for hw being set st hw in Pmin & h c= hw holds
Pb \/ {h} is_finer_than Pmin ) )

A6: now :: thesis: for s being set st s in Pmax & h c= s holds
h = s
let s be set ; :: thesis: ( s in Pmax & h c= s implies h = s )
assume that
A7: s in Pmax and
A8: h c= s ; :: thesis: h = s
consider hy being set such that
A9: hy in Pmax and
A10: hy c= h by A4;
hy <> {} by ;
then hy meets s by ;
then s = hy by ;
hence h = s by ; :: thesis: verum
end;
let Pb be set ; :: thesis: ( ( for x being set holds
( x in Pb iff ( x in Pmax & x misses h ) ) ) implies ( Pb \/ {h} is a_partition of X & Pmax is_finer_than Pb \/ {h} & ( for Pmin being a_partition of X st Pmax is_finer_than Pmin holds
for hw being set st hw in Pmin & h c= hw holds
Pb \/ {h} is_finer_than Pmin ) ) )

assume A11: for x being set holds
( x in Pb iff ( x in Pmax & x misses h ) ) ; :: thesis: ( Pb \/ {h} is a_partition of X & Pmax is_finer_than Pb \/ {h} & ( for Pmin being a_partition of X st Pmax is_finer_than Pmin holds
for hw being set st hw in Pmin & h c= hw holds
Pb \/ {h} is_finer_than Pmin ) )

set P = Pb \/ {h};
A12: Pb c= Pb \/ {h} by XBOOLE_1:7;
A13: Pb c= Pmax by A11;
A14: now :: thesis: for A being Subset of X st A in Pb \/ {h} holds
( A <> {} & ( for B being Subset of X holds
( not B in Pb \/ {h} or A = B or A misses B ) ) )
let A be Subset of X; :: thesis: ( A in Pb \/ {h} implies ( A <> {} & ( for B being Subset of X holds
( not B in Pb \/ {h} or A = B or A misses B ) ) ) )

assume A15: A in Pb \/ {h} ; :: thesis: ( A <> {} & ( for B being Subset of X holds
( not B in Pb \/ {h} or A = B or A misses B ) ) )

now :: thesis: A <> {} end;
hence A <> {} ; :: thesis: for B being Subset of X holds
( not B in Pb \/ {h} or A = B or A misses B )

thus for B being Subset of X holds
( not B in Pb \/ {h} or A = B or A misses B ) :: thesis: verum
proof
let B be Subset of X; :: thesis: ( not B in Pb \/ {h} or A = B or A misses B )
assume A16: B in Pb \/ {h} ; :: thesis: ( A = B or A misses B )
per cases ( A in Pb or A in {h} ) by ;
suppose A17: A in Pb ; :: thesis: ( A = B or A misses B )
per cases ( B in Pb or B in {h} ) by ;
suppose B in Pb ; :: thesis: ( A = B or A misses B )
hence ( A = B or A misses B ) by ; :: thesis: verum
end;
suppose B in {h} ; :: thesis: ( A = B or A misses B )
then B = h by TARSKI:def 1;
hence ( A = B or A misses B ) by ; :: thesis: verum
end;
end;
end;
suppose A18: A in {h} ; :: thesis: ( A = B or A misses B )
per cases ( B in Pb or B in {h} ) by ;
suppose A19: B in Pb ; :: thesis: ( A = B or A misses B )
A = h by ;
hence ( A = B or A misses B ) by ; :: thesis: verum
end;
suppose B in {h} ; :: thesis: ( A = B or A misses B )
then B = h by TARSKI:def 1;
hence ( A = B or A misses B ) by ; :: thesis: verum
end;
end;
end;
end;
end;
end;
A20: {h} c= Pb \/ {h} by XBOOLE_1:7;
A21: union Pmax = X by EQREL_1:def 4;
A22: X c= union (Pb \/ {h})
proof
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in X or s in union (Pb \/ {h}) )
assume s in X ; :: thesis: s in union (Pb \/ {h})
then consider t being set such that
A23: s in t and
A24: t in Pmax by ;
per cases ( t in Pb or not t in Pb ) ;
suppose t in Pb ; :: thesis: s in union (Pb \/ {h})
hence s in union (Pb \/ {h}) by ; :: thesis: verum
end;
end;
end;
Pb c= bool X by ;
then A27: Pb \/ {h} c= bool X by ;
union (Pb \/ {h}) c= X
proof
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in union (Pb \/ {h}) or s in X )
assume s in union (Pb \/ {h}) ; :: thesis: s in X
then ex t being set st
( s in t & t in Pb \/ {h} ) by TARSKI:def 4;
hence s in X by A27; :: thesis: verum
end;
then union (Pb \/ {h}) = X by ;
hence Pb \/ {h} is a_partition of X by ; :: thesis: ( Pmax is_finer_than Pb \/ {h} & ( for Pmin being a_partition of X st Pmax is_finer_than Pmin holds
for hw being set st hw in Pmin & h c= hw holds
Pb \/ {h} is_finer_than Pmin ) )

thus Pmax is_finer_than Pb \/ {h} :: thesis: for Pmin being a_partition of X st Pmax is_finer_than Pmin holds
for hw being set st hw in Pmin & h c= hw holds
Pb \/ {h} is_finer_than Pmin
proof
let x be set ; :: according to SETFAM_1:def 2 :: thesis: ( not x in Pmax or ex b1 being set st
( b1 in Pb \/ {h} & x c= b1 ) )

assume A28: x in Pmax ; :: thesis: ex b1 being set st
( b1 in Pb \/ {h} & x c= b1 )

per cases ( x c= h or not x c= h ) ;
suppose x c= h ; :: thesis: ex b1 being set st
( b1 in Pb \/ {h} & x c= b1 )

hence ex b1 being set st
( b1 in Pb \/ {h} & x c= b1 ) by ; :: thesis: verum
end;
suppose A29: not x c= h ; :: thesis: ex b1 being set st
( b1 in Pb \/ {h} & x c= b1 )

per cases ( h c= x or h misses x ) by A5, A28, A29;
suppose h c= x ; :: thesis: ex b1 being set st
( b1 in Pb \/ {h} & x c= b1 )

then h = x by ;
hence ex b1 being set st
( b1 in Pb \/ {h} & x c= b1 ) by ; :: thesis: verum
end;
suppose h misses x ; :: thesis: ex b1 being set st
( b1 in Pb \/ {h} & x c= b1 )

then x in Pb by ;
hence ex b1 being set st
( b1 in Pb \/ {h} & x c= b1 ) by A12; :: thesis: verum
end;
end;
end;
end;
end;
let Pmin be a_partition of X; :: thesis: ( Pmax is_finer_than Pmin implies for hw being set st hw in Pmin & h c= hw holds
Pb \/ {h} is_finer_than Pmin )

assume A30: Pmax is_finer_than Pmin ; :: thesis: for hw being set st hw in Pmin & h c= hw holds
Pb \/ {h} is_finer_than Pmin

let hw be set ; :: thesis: ( hw in Pmin & h c= hw implies Pb \/ {h} is_finer_than Pmin )
assume that
A31: hw in Pmin and
A32: h c= hw ; :: thesis: Pb \/ {h} is_finer_than Pmin
let s be set ; :: according to SETFAM_1:def 2 :: thesis: ( not s in Pb \/ {h} or ex b1 being set st
( b1 in Pmin & s c= b1 ) )

assume A33: s in Pb \/ {h} ; :: thesis: ex b1 being set st
( b1 in Pmin & s c= b1 )

per cases ( s in Pb or s in {h} ) by ;
suppose s in Pb ; :: thesis: ex b1 being set st
( b1 in Pmin & s c= b1 )

then s in Pmax by A11;
hence ex b1 being set st
( b1 in Pmin & s c= b1 ) by A30; :: thesis: verum
end;
suppose s in {h} ; :: thesis: ex b1 being set st
( b1 in Pmin & s c= b1 )

then s = h by TARSKI:def 1;
hence ex b1 being set st
( b1 in Pmin & s c= b1 ) by ; :: thesis: verum
end;
end;