let X, h be non empty set ; :: thesis:
assume A1: h c= X ; :: thesis:
let Pmax be a_partition of X; :: thesis:
assume that
A2: ex hy being set st
( hy in Pmax & hy c= h ) and
A3: for x being set holds
( not x in Pmax or x c= h or h c= x or h misses x ) ; :: thesis:
A4: union Pmax = X by EQREL_1:def 6;
let Pb be set ; :: thesis:
assume A5: for x being set holds
( x in Pb iff ( x in Pmax & x misses h ) ) ; :: thesis:
set P = Pb \/ {h};
A6: Pb c= Pb \/ {h} by XBOOLE_1:7;
A7: h in {h} by TARSKI:def 1;
A8: {h} c= Pb \/ {h} by XBOOLE_1:7;

A9: now

let s be set ; :: thesis:
assume A10: ( s in Pmax & h c= s ) ; :: thesis:
consider hy being set such that
A11: ( hy in Pmax & hy c= h ) by A2;
hy <> {} by A11, EQREL_1:def 6;
then hy meets s by A10, A11, Lm4, XBOOLE_1:1;
then s = hy by A10, A11, EQREL_1:def 6;
hence h = s by A10, A11, XBOOLE_0:def 10; :: thesis:

end;

A12: Pb c= Pmax

proof

let s be set ; :: according to TARSKI:def 3 :: thesis:
assume A13: s in Pb ; :: thesis:
thus s in Pmax by A5, A13; :: thesis:

end;

then A14: Pb c= bool X by XBOOLE_1:1;
{h} c= bool X

proof

let s be set ; :: according to TARSKI:def 3 :: thesis:
assume s in {h} ; :: thesis:
then s = h by TARSKI:def 1;
hence s in bool X by A1; :: thesis:

end;

then A15: Pb \/ {h} c= bool X by A14, XBOOLE_1:8;
A16: union (Pb \/ {h}) = X

proof

thus union (Pb \/ {h}) c= X :: according to XBOOLE_0:def 10 :: thesis:

proof

let s be set ; :: according to TARSKI:def 3 :: thesis:
assume A17: s in union (Pb \/ {h}) ; :: thesis:
consider t being set such that
A18: ( s in t & t in Pb \/ {h} ) by A17, TARSKI:def 4;
thus s in X by A15, A18; :: thesis:

end;

thus X c= union (Pb \/ {h}) :: thesis:

proof

let s be set ; :: according to TARSKI:def 3 :: thesis:
assume A19: s in X ; :: thesis:
consider t being set such that
A20: ( s in t & t in Pmax ) by A4, A19, TARSKI:def 4;

per cases ;

suppose t in Pb ; :: thesis:

hence s in union (Pb \/ {h}) by A6, A20, TARSKI:def 4; :: thesis:

end;

suppose not t in Pb ; :: thesis:

then A21: t meets h by A5, A20;

per cases by A3, A20, A21;

suppose h c= t ; :: thesis:

then t = h by A9, A20;
hence s in union (Pb \/ {h}) by A7, A8, A20, TARSKI:def 4; :: thesis:

end;

suppose A22: t c= h ; :: thesis:

h in {h} by TARSKI:def 1;
hence s in union (Pb \/ {h}) by A8, A20, A22, TARSKI:def 4; :: thesis:

end;

now

let A be Subset of X; :: thesis:
assume A23: A in Pb \/ {h} ; :: thesis:

now

per cases by A23, XBOOLE_0:def 3;

suppose A in Pb ; :: thesis:

then A in Pmax by A5;
hence A <> {} by EQREL_1:def 6; :: thesis:

end;

suppose A in {h} ; :: thesis:

hence A <> {} by TARSKI:def 1; :: thesis:

end;

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

proof

let B be Subset of X; :: thesis:
assume A24: B in Pb \/ {h} ; :: thesis:

per cases by A23, XBOOLE_0:def 3;

suppose A25: A in Pb ; :: thesis:

per cases by A24, XBOOLE_0:def 3;

suppose B in Pb ; :: thesis:

hence ( A = B or A misses B ) by A12, A25, EQREL_1:def 6; :: thesis:

end;

suppose B in {h} ; :: thesis:

then B = h by TARSKI:def 1;
hence ( A = B or A misses B ) by A5, A25; :: thesis:

end;

suppose A26: A in {h} ; :: thesis:

per cases by A24, XBOOLE_0:def 3;

suppose A27: B in Pb ; :: thesis:

A = h by A26, TARSKI:def 1;
hence ( A = B or A misses B ) by A5, A27; :: thesis:

end;

suppose B in {h} ; :: thesis:

then B = h by TARSKI:def 1;
hence ( A = B or A misses B ) by A26, TARSKI:def 1; :: thesis:

end;

hence Pb \/ {h} is a_partition of X by A15, A16, EQREL_1:def 6; :: thesis:
thus Pmax is_finer_than Pb \/ {h} :: thesis:

proof

let x be set ; :: according to SETFAM_1:def 2 :: thesis:
assume A28: x in Pmax ; :: thesis:

per cases ;

suppose x c= h ; :: thesis:

hence ex b₁ being set st
( b₁ in Pb \/ {h} & x c= b₁ ) by A7, A8; :: thesis:

end;

suppose A29: not x c= h ; :: thesis:

per cases by A3, A28, A29;

suppose h c= x ; :: thesis:

then h = x by A9, A28;
hence ex b₁ being set st
( b₁ in Pb \/ {h} & x c= b₁ ) by A7, A8; :: thesis:

end;

suppose h misses x ; :: thesis:

then x in Pb by A5, A28;
hence ex b₁ being set st
( b₁ in Pb \/ {h} & x c= b₁ ) by A6; :: thesis:

end;

let Pmin be a_partition of X; :: thesis:
assume A30: Pmax is_finer_than Pmin ; :: thesis:
let hw be set ; :: thesis:
assume A31: ( hw in Pmin & h c= hw ) ; :: thesis:
let s be set ; :: according to SETFAM_1:def 2 :: thesis:
assume A32: s in Pb \/ {h} ; :: thesis:

per cases by A32, XBOOLE_0:def 3;

suppose s in Pb ; :: thesis:

then s in Pmax by A5;
then consider t being set such that
A33: ( t in Pmin & s c= t ) by A30, SETFAM_1:def 2;
thus ex b₁ being set st
( b₁ in Pmin & s c= b₁ ) by A33; :: thesis:

end;

suppose s in {h} ; :: thesis:

then s = h by TARSKI:def 1;
hence ex b₁ being set st
( b₁ in Pmin & s c= b₁ ) by A31; :: thesis:

end;