let X, h be non empty set ; :: thesis:
let Pmin be a_partition of X; :: thesis:
let hw be set ; :: thesis:
assume that
A1: hw in Pmin and
A2: h c= hw ; :: thesis:
let PS be a_partition of X; :: thesis:
assume that
A3: h in PS and
A4: for x being set holds
( not x in PS or x c= hw or hw c= x or hw misses x ) ; :: thesis:
let PT be set ; :: thesis:
assume A5: for a being set holds
( a in PT iff ( a in PS & a c= hw ) ) ; :: thesis:
A6: PT c= PS by A5;
A7: union PS = X by EQREL_1:def 4;
A8: union Pmin = X by EQREL_1:def 4;
set P = PT \/ (Pmin \ {hw});
A9: PT c= PT \/ (Pmin \ {hw}) by XBOOLE_1:7;
A10: Pmin \ {hw} c= PT \/ (Pmin \ {hw}) by XBOOLE_1:7;
A11: h in PT by A2, A3, A5;
A12: X c= union (PT \/ (Pmin \ {hw}))

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume A13: a in X ; :: thesis:
consider b being set such that
A14: a in b and
A15: b in Pmin by A8, A13, TARSKI:def 4;

per cases ;

suppose A16: b = hw ; :: thesis:

consider c being set such that
A17: a in c and
A18: c in PS by A7, A13, TARSKI:def 4;
A19: hw meets c by A14, A16, A17, XBOOLE_0:3;

per cases by A4, A18, A19;

suppose hw c= c ; :: thesis:

then A20: h c= c by A2;
h meets c

proof

A21: ex x being object st x in h by XBOOLE_0:def 1;
assume h misses c ; :: thesis:
hence contradiction by A20, A21, XBOOLE_0:3; :: thesis:

end;

then h = c by A3, A18, EQREL_1:def 4;
hence a in union (PT \/ (Pmin \ {hw})) by A9, A11, A17, TARSKI:def 4; :: thesis:

end;

suppose c c= hw ; :: thesis:

then c in PT by A5, A18;
hence a in union (PT \/ (Pmin \ {hw})) by A9, A17, TARSKI:def 4; :: thesis:

end;

end;

end;

suppose b <> hw ; :: thesis:

then not b in {hw} by TARSKI:def 1;
then b in Pmin \ {hw} by A15, XBOOLE_0:def 5;
hence a in union (PT \/ (Pmin \ {hw})) by A10, A14, TARSKI:def 4; :: thesis:

end;

end;

end;

A22: Pmin \ {hw} c= Pmin by XBOOLE_1:36;

A23: now :: thesis:

let x, y be set ; :: thesis:
assume that
A24: x in PT and
A25: y in Pmin \ {hw} ; :: thesis:
A26: y in Pmin by A25, XBOOLE_0:def 5;
not y in {hw} by A25, XBOOLE_0:def 5;
then A27: y <> hw by TARSKI:def 1;
A28: x c= hw by A5, A24;

now :: thesis:

assume x meets y ; :: thesis:
then ex a being object st
( a in x & a in y ) by XBOOLE_0:3;
then hw meets y by A28, XBOOLE_0:3;
hence contradiction by A1, A26, A27, EQREL_1:def 4; :: thesis:

end;

hence x misses y ; :: thesis:

end;

A29: now :: thesis:

let A be Subset of X; :: thesis:
assume A30: A in PT \/ (Pmin \ {hw}) ; :: thesis:

now :: thesis:

per cases by A30, XBOOLE_0:def 3;

suppose A in PT ; :: thesis:

hence A <> {} by A6, EQREL_1:def 4; :: thesis:

end;

suppose A in Pmin \ {hw} ; :: thesis:

hence A <> {} by A22, EQREL_1:def 4; :: thesis:

end;

end;

end;

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

proof

let B be Subset of X; :: thesis:
assume A31: B in PT \/ (Pmin \ {hw}) ; :: thesis:

per cases by A30, XBOOLE_0:def 3;

suppose A32: A in PT ; :: thesis:

per cases by A31, XBOOLE_0:def 3;

suppose B in PT ; :: thesis:

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

end;

suppose B in Pmin \ {hw} ; :: thesis:

hence ( A = B or A misses B ) by A23, A32; :: thesis:

end;

end;

end;

suppose A33: A in Pmin \ {hw} ; :: thesis:

per cases by A31, XBOOLE_0:def 3;

suppose B in PT ; :: thesis:

hence ( A = B or A misses B ) by A23, A33; :: thesis:

end;

suppose B in Pmin \ {hw} ; :: thesis:

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

end;

end;

end;

end;

end;

end;

PT c= bool X by A6, XBOOLE_1:1;
then A34: PT \/ (Pmin \ {hw}) c= bool X by XBOOLE_1:8;
union (PT \/ (Pmin \ {hw})) c= X

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in union (PT \/ (Pmin \ {hw})) ; :: thesis:
then ex b being set st
( a in b & b in PT \/ (Pmin \ {hw}) ) by TARSKI:def 4;
hence a in X by A34; :: thesis:

end;

then union (PT \/ (Pmin \ {hw})) = X by A12, XBOOLE_0:def 10;
hence PT \/ (Pmin \ {hw}) is a_partition of X by A34, A29, EQREL_1:def 4; :: thesis:
let a be set ; :: according to SETFAM_1:def 2 :: thesis:
assume A35: a in PT \/ (Pmin \ {hw}) ; :: thesis:

per cases by A35, XBOOLE_0:def 3;

suppose a in PT ; :: thesis:

then a c= hw by A5;
hence ex b₁ being set st
( b₁ in Pmin & a c= b₁ ) by A1; :: thesis:

end;

suppose a in Pmin \ {hw} ; :: thesis:

hence ex b₁ being set st
( b₁ in Pmin & a c= b₁ ) by A22; :: thesis:

end;

end;