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}))

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

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

hence PT \/ (Pmin \ {hw}) is a_partition of X by A34, A29, EQREL_1:def 4; :: 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 b_{1} being set st

( b_{1} in Pmin & a c= b_{1} ) )

assume A35: a in PT \/ (Pmin \ {hw}) ; :: thesis: ex b_{1} being set st

( b_{1} in Pmin & a c= b_{1} )

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

A22:
Pmin \ {hw} c= Pmin
by XBOOLE_1:36;
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 A8, A13, TARSKI:def 4;

end;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 A8, A13, TARSKI:def 4;

per cases
( b = hw or b <> hw )
;

end;

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 A7, A13, TARSKI:def 4;

A19: hw meets c by A14, A16, A17, XBOOLE_0:3;

end;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
( hw c= c or c c= hw )
by A4, A18, A19;

end;

suppose
hw c= c
; :: thesis: a in union (PT \/ (Pmin \ {hw}))

then A20:
h c= c
by A2;

h meets c

hence a in union (PT \/ (Pmin \ {hw})) by A9, A11, A17, TARSKI:def 4; :: thesis: verum

end;h meets c

proof

then
h = c
by A3, A18, EQREL_1:def 4;
A21:
ex x being object st x in h
by XBOOLE_0:def 1;

assume h misses c ; :: thesis: contradiction

hence contradiction by A20, A21, XBOOLE_0:3; :: thesis: verum

end;assume h misses c ; :: thesis: contradiction

hence contradiction by A20, A21, XBOOLE_0:3; :: thesis: verum

hence a in union (PT \/ (Pmin \ {hw})) by A9, A11, A17, TARSKI:def 4; :: thesis: verum

A23: now :: thesis: for x, y being set st x in PT & y in Pmin \ {hw} holds

x misses y

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 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;

end;assume that

A24: x in PT and

A25: y in Pmin \ {hw} ; :: thesis: x misses y

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: not x meets y

hence
x misses y
; :: thesis: verumassume
x meets y
; :: thesis: contradiction

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: verum

end;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: verum

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 ) ) )

PT c= bool X
by A6, XBOOLE_1:1;( 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 ) ) )

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

end;( 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 ) ) )

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 )

end;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 A30, XBOOLE_0:def 3;

end;

suppose A32:
A in PT
; :: thesis: ( A = B or A misses B )

end;

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

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

proof

then
union (PT \/ (Pmin \ {hw})) = X
by A12, XBOOLE_0:def 10;
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;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

hence PT \/ (Pmin \ {hw}) is a_partition of X by A34, A29, EQREL_1:def 4; :: 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 b

( b

assume A35: a in PT \/ (Pmin \ {hw}) ; :: thesis: ex b

( b