let X, h be non empty set ; :: thesis:
assume A1: h c= X ; :: thesis:
A2: {h} c= bool X

proof

let s be object ; :: 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;

A3: h in {h} by TARSKI:def 1;
let Pmax be a_partition of X; :: thesis:
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:

A6: now :: thesis:

let s be set ; :: thesis:
assume that
A7: s in Pmax and
A8: h c= s ; :: thesis:
consider hy being set such that
A9: hy in Pmax and
A10: hy c= h by A4;
hy <> {} by A9, EQREL_1:def 4;
then hy meets s by A8, A10, Lm5, XBOOLE_1:1;
then s = hy by A7, A9, EQREL_1:def 4;
hence h = s by A8, A10, XBOOLE_0:def 10; :: thesis:

end;

let Pb be set ; :: thesis:
assume A11: for x being set holds
( x in Pb iff ( x in Pmax & x misses h ) ) ; :: thesis:
set P = Pb \/ {h};
A12: Pb c= Pb \/ {h} by XBOOLE_1:7;
A13: Pb c= Pmax by A11;

A14: now :: thesis:

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

now :: thesis:

per cases by A15, XBOOLE_0:def 3;

suppose A in Pb ; :: thesis:

then A in Pmax by A11;
hence A <> {} by EQREL_1:def 4; :: thesis:

end;

suppose A in {h} ; :: thesis:

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

end;

end;

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 A16: B in Pb \/ {h} ; :: thesis:

per cases by A15, XBOOLE_0:def 3;

suppose A17: A in Pb ; :: thesis:

per cases by A16, XBOOLE_0:def 3;

suppose B in Pb ; :: thesis:

hence ( A = B or A misses B ) by A13, A17, EQREL_1:def 4; :: thesis:

end;

suppose B in {h} ; :: thesis:

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

end;

end;

end;

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

per cases by A16, XBOOLE_0:def 3;

suppose A19: B in Pb ; :: thesis:

A = h by A18, TARSKI:def 1;
hence ( A = B or A misses B ) by A11, A19; :: thesis:

end;

suppose B in {h} ; :: thesis:

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

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:
assume s in X ; :: thesis:
then consider t being set such that
A23: s in t and
A24: t in Pmax by A21, TARSKI:def 4;

per cases ;

suppose t in Pb ; :: thesis:

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

end;

suppose not t in Pb ; :: thesis:

then A25: t meets h by A11, A24;

per cases by A5, A24, A25;

suppose h c= t ; :: thesis:

then t = h by A6, A24;
hence s in union (Pb \/ {h}) by A3, A20, A23, TARSKI:def 4; :: thesis:

end;

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

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

end;

end;

end;

end;

end;

Pb c= bool X by A13, XBOOLE_1:1;
then A27: Pb \/ {h} c= bool X by A2, XBOOLE_1:8;
union (Pb \/ {h}) c= X

proof

let s be object ; :: according to TARSKI:def 3 :: thesis:
assume s in union (Pb \/ {h}) ; :: thesis:
then ex t being set st
( s in t & t in Pb \/ {h} ) by TARSKI:def 4;
hence s in X by A27; :: thesis:

end;

then union (Pb \/ {h}) = X by A22, XBOOLE_0:def 10;
hence Pb \/ {h} is a_partition of X by A27, A14, EQREL_1:def 4; :: 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 A3, A20; :: thesis:

end;

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

per cases by A5, A28, A29;

suppose h c= x ; :: thesis:

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

end;

suppose h misses x ; :: thesis:

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

end;

end;

end;

end;

end;

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

per cases by A33, XBOOLE_0:def 3;

suppose s in Pb ; :: thesis:

then s in Pmax by A11;
hence ex b₁ being set st
( b₁ in Pmin & s c= b₁ ) by A30; :: 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, A32; :: thesis:

end;

end;