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

let Pmin be a_partition of X; :: thesis: for hw being set st hw in Pmin & h c= hw holds
for PS being a_partition of X st h in PS & ( for x being set holds
( not x in PS or x c= hw or hw c= x or hw misses x ) ) holds
for PT being set st ( for a being set holds
( a in PT iff ( a in PS & a c= hw ) ) ) holds
( PT \/ (Pmin \ {hw}) is a_partition of X & PT \/ (Pmin \ {hw}) is_finer_than Pmin )

let hw be set ; :: thesis: ( hw in Pmin & h c= hw implies for PS being a_partition of X st h in PS & ( for x being set holds
( not x in PS or x c= hw or hw c= x or hw misses x ) ) holds
for PT being set st ( for a being set holds
( a in PT iff ( a in PS & a c= hw ) ) ) holds
( PT \/ (Pmin \ {hw}) is a_partition of X & PT \/ (Pmin \ {hw}) is_finer_than Pmin ) )

assume that
A1: hw in Pmin and
A2: h c= hw ; :: thesis: for PS being a_partition of X st h in PS & ( for x being set holds
( not x in PS or x c= hw or hw c= x or hw misses x ) ) holds
for PT being set st ( for a being set holds
( a in PT iff ( a in PS & a c= hw ) ) ) holds
( PT \/ (Pmin \ {hw}) is a_partition of X & PT \/ (Pmin \ {hw}) is_finer_than Pmin )

let PS be a_partition of X; :: thesis: ( h in PS & ( for x being set holds
( not x in PS or x c= hw or hw c= x or hw misses x ) ) implies for PT being set st ( for a being set holds
( a in PT iff ( a in PS & a c= hw ) ) ) holds
( PT \/ (Pmin \ {hw}) is a_partition of X & PT \/ (Pmin \ {hw}) is_finer_than Pmin ) )

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: for PT being set st ( for a being set holds
( a in PT iff ( a in PS & a c= hw ) ) ) holds
( PT \/ (Pmin \ {hw}) is a_partition of X & PT \/ (Pmin \ {hw}) is_finer_than Pmin )

let PT be set ; :: thesis: ( ( for a being set holds
( a in PT iff ( a in PS & a c= hw ) ) ) implies ( PT \/ (Pmin \ {hw}) is a_partition of X & PT \/ (Pmin \ {hw}) is_finer_than Pmin ) )

assume A5: for a being set holds
( a in PT iff ( a in PS & a c= hw ) ) ; :: thesis: ( PT \/ (Pmin \ {hw}) is a_partition of X & PT \/ (Pmin \ {hw}) is_finer_than Pmin )
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: ( not a in X or a in union (PT \/ (Pmin \ {hw})) )
assume A13: a in X ; :: thesis: a in union (PT \/ (Pmin \ {hw}))
consider b being set such that
A14: a in b and
A15: b in Pmin by ;
per cases ( b = hw or b <> hw ) ;
suppose A16: b = hw ; :: thesis: a in union (PT \/ (Pmin \ {hw}))
consider c being set such that
A17: a in c and
A18: c in PS by ;
A19: hw meets c by ;
per cases ( hw c= c or c c= hw ) by A4, A18, A19;
suppose hw c= c ; :: thesis: a in union (PT \/ (Pmin \ {hw}))
end;
suppose c c= hw ; :: thesis: a in union (PT \/ (Pmin \ {hw}))
then c in PT by ;
hence a in union (PT \/ (Pmin \ {hw})) by ; :: thesis: verum
end;
end;
end;
suppose b <> hw ; :: thesis: a in union (PT \/ (Pmin \ {hw}))
then not b in {hw} by TARSKI:def 1;
then b in Pmin \ {hw} by ;
hence a in union (PT \/ (Pmin \ {hw})) by ; :: thesis: verum
end;
end;
end;
A22: Pmin \ {hw} c= Pmin by XBOOLE_1:36;
A23: now :: thesis: for x, y being set st x in PT & y in Pmin \ {hw} holds
x misses y
let x, y be set ; :: thesis: ( x in PT & y in Pmin \ {hw} implies x misses y )
assume that
A24: x in PT and
A25: y in Pmin \ {hw} ; :: thesis: x misses y
A26: y in Pmin by ;
not y in {hw} by ;
then A27: y <> hw by TARSKI:def 1;
A28: x c= hw by ;
now :: thesis: not x meets yend;
hence x misses y ; :: thesis: verum
end;
A29: now :: thesis: for A being Subset of X st A in PT \/ (Pmin \ {hw}) holds
( A <> {} & ( for B being Subset of X holds
( not B in PT \/ (Pmin \ {hw}) or A = B or A misses B ) ) )
let A be Subset of X; :: thesis: ( A in PT \/ (Pmin \ {hw}) implies ( A <> {} & ( for B being Subset of X holds
( not B in PT \/ (Pmin \ {hw}) or A = B or A misses B ) ) ) )

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

now :: thesis: A <> {}
per cases ( A in PT or A in Pmin \ {hw} ) by ;
suppose A in Pmin \ {hw} ; :: thesis: A <> {}
hence A <> {} by ; :: thesis: verum
end;
end;
end;
hence A <> {} ; :: thesis: for B being Subset of X holds
( not B in PT \/ (Pmin \ {hw}) or A = B or A misses B )

thus for B being Subset of X holds
( not B in PT \/ (Pmin \ {hw}) or A = B or A misses B ) :: thesis: verum
proof
let B be Subset of X; :: thesis: ( not B in PT \/ (Pmin \ {hw}) or A = B or A misses B )
assume A31: B in PT \/ (Pmin \ {hw}) ; :: thesis: ( A = B or A misses B )
per cases ( A in PT or A in Pmin \ {hw} ) by ;
suppose A32: A in PT ; :: thesis: ( A = B or A misses B )
per cases ( B in PT or B in Pmin \ {hw} ) by ;
suppose B in PT ; :: thesis: ( A = B or A misses B )
hence ( A = B or A misses B ) by ; :: thesis: verum
end;
suppose B in Pmin \ {hw} ; :: thesis: ( A = B or A misses B )
hence ( A = B or A misses B ) by ; :: thesis: verum
end;
end;
end;
suppose A33: A in Pmin \ {hw} ; :: thesis: ( A = B or A misses B )
per cases ( B in PT or B in Pmin \ {hw} ) by ;
suppose B in PT ; :: thesis: ( A = B or A misses B )
hence ( A = B or A misses B ) by ; :: thesis: verum
end;
suppose B in Pmin \ {hw} ; :: thesis: ( A = B or A misses B )
hence ( A = B or A misses B ) by ; :: thesis: verum
end;
end;
end;
end;
end;
end;
PT c= bool X by ;
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: ( not a in union (PT \/ (Pmin \ {hw})) or a in X )
assume a in union (PT \/ (Pmin \ {hw})) ; :: thesis: a in X
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: verum
end;
then union (PT \/ (Pmin \ {hw})) = X by ;
hence PT \/ (Pmin \ {hw}) is a_partition of X by ; :: thesis: PT \/ (Pmin \ {hw}) is_finer_than Pmin
let a be set ; :: according to SETFAM_1:def 2 :: thesis: ( not a in PT \/ (Pmin \ {hw}) or ex b1 being set st
( b1 in Pmin & a c= b1 ) )

assume A35: a in PT \/ (Pmin \ {hw}) ; :: thesis: ex b1 being set st
( b1 in Pmin & a c= b1 )

per cases ( a in PT or a in Pmin \ {hw} ) by ;
suppose a in PT ; :: thesis: ex b1 being set st
( b1 in Pmin & a c= b1 )

then a c= hw by A5;
hence ex b1 being set st
( b1 in Pmin & a c= b1 ) by A1; :: thesis: verum
end;
suppose a in Pmin \ {hw} ; :: thesis: ex b1 being set st
( b1 in Pmin & a c= b1 )

hence ex b1 being set st
( b1 in Pmin & a c= b1 ) by A22; :: thesis: verum
end;
end;