let X, h be non empty set ; :: thesis:
let Pmin be a_partition of X; :: thesis:
let hw be set ; :: thesis:
assume A1: ( hw in Pmin & h c= hw ) ; :: thesis:
let PS be a_partition of X; :: thesis:
assume that
A2: h in PS and
A3: 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 A4: for a being set holds
( a in PT iff ( a in PS & a c= hw ) ) ; :: thesis:
A5: union Pmin = X by EQREL_1:def 6;
A6: union PS = X by EQREL_1:def 6;
set P = PT \/ (Pmin \ {hw});
A7: PT c= PT \/ (Pmin \ {hw}) by XBOOLE_1:7;
A8: h in PT by A1, A2, A4;
A9: Pmin \ {hw} c= PT \/ (Pmin \ {hw}) by XBOOLE_1:7;
A10: PT c= PS

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume A11: a in PT ; :: thesis:
thus a in PS by A4, A11; :: thesis:

end;

then A12: PT c= bool X by XBOOLE_1:1;
A13: Pmin \ {hw} c= Pmin by XBOOLE_1:36;
A14: PT \/ (Pmin \ {hw}) c= bool X by A12, XBOOLE_1:8;

A15: now

let x, y be set ; :: thesis:
assume A16: ( x in PT & y in Pmin \ {hw} ) ; :: thesis:
A17: x c= hw by A4, A16;
A18: ( y in Pmin & not y in {hw} ) by A16, XBOOLE_0:def 5;
then A19: y <> hw by TARSKI:def 1;

now

assume x meets y ; :: thesis:
then consider a being set such that
A20: ( a in x & a in y ) by XBOOLE_0:3;
hw meets y by A17, A20, XBOOLE_0:3;
hence contradiction by A1, A18, A19, EQREL_1:def 6; :: thesis:

end;

hence x misses y ; :: thesis:

end;

A21: union (PT \/ (Pmin \ {hw})) = X

proof

thus union (PT \/ (Pmin \ {hw})) c= X :: according to XBOOLE_0:def 10 :: thesis:

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume A22: a in union (PT \/ (Pmin \ {hw})) ; :: thesis:
consider b being set such that
A23: ( a in b & b in PT \/ (Pmin \ {hw}) ) by A22, TARSKI:def 4;
thus a in X by A14, A23; :: thesis:

end;

thus X c= union (PT \/ (Pmin \ {hw})) :: thesis:

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume A24: a in X ; :: thesis:
consider b being set such that
A25: ( a in b & b in Pmin ) by A5, A24, TARSKI:def 4;

per cases ;

suppose A26: b = hw ; :: thesis:

consider c being set such that
A27: ( a in c & c in PS ) by A6, A24, TARSKI:def 4;
A28: hw meets c by A25, A26, A27, XBOOLE_0:3;

per cases by A3, A27, A28;

suppose hw c= c ; :: thesis:

then A29: h c= c by A1, XBOOLE_1:1;
h meets c

proof

assume A30: h misses c ; :: thesis:
consider x being set such that
A31: x in h by XBOOLE_0:def 1;
thus contradiction by A29, A30, A31, XBOOLE_0:3; :: thesis:

end;

then h = c by A2, A27, EQREL_1:def 6;
hence a in union (PT \/ (Pmin \ {hw})) by A7, A8, A27, TARSKI:def 4; :: thesis:

end;

suppose c c= hw ; :: thesis:

then c in PT by A4, A27;
hence a in union (PT \/ (Pmin \ {hw})) by A7, A27, TARSKI:def 4; :: thesis:

end;

suppose b <> hw ; :: thesis:

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

end;

now

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

now

per cases by A32, XBOOLE_0:def 3;

suppose A in PT ; :: thesis:

hence A <> {} by A10, EQREL_1:def 6; :: thesis:

end;

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

hence A <> {} by A13, EQREL_1:def 6; :: thesis:

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 A33: B in PT \/ (Pmin \ {hw}) ; :: thesis:

per cases by A32, XBOOLE_0:def 3;

suppose A34: A in PT ; :: thesis:

per cases by A33, XBOOLE_0:def 3;

suppose B in PT ; :: thesis:

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

end;

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

hence ( A = B or A misses B ) by A15, A34; :: thesis:

end;

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

per cases by A33, XBOOLE_0:def 3;

suppose B in PT ; :: thesis:

hence ( A = B or A misses B ) by A15, A35; :: thesis:

end;

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

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

end;

hence PT \/ (Pmin \ {hw}) is a_partition of X by A14, A21, EQREL_1:def 6; :: thesis:
let a be set ; :: according to SETFAM_1:def 2 :: thesis:
assume A36: a in PT \/ (Pmin \ {hw}) ; :: thesis:

per cases by A36, XBOOLE_0:def 3;

suppose a in PT ; :: thesis:

then a c= hw by A4;
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 A13; :: thesis:

end;