let X, h be non empty set ; :: thesis: ( h c= X implies for Pmax being a_partition of X st ex hy being set st

( hy in Pmax & hy c= h ) & ( for x being set holds

( not x in Pmax or x c= h or h c= x or h misses x ) ) holds

for Pb being set st ( for x being set holds

( x in Pb iff ( x in Pmax & x misses h ) ) ) holds

( Pb \/ {h} is a_partition of X & Pmax is_finer_than Pb \/ {h} & ( for Pmin being a_partition of X st Pmax is_finer_than Pmin holds

for hw being set st hw in Pmin & h c= hw holds

Pb \/ {h} is_finer_than Pmin ) ) )

assume A1: h c= X ; :: thesis: for Pmax being a_partition of X st ex hy being set st

( hy in Pmax & hy c= h ) & ( for x being set holds

( not x in Pmax or x c= h or h c= x or h misses x ) ) holds

for Pb being set st ( for x being set holds

( x in Pb iff ( x in Pmax & x misses h ) ) ) holds

( Pb \/ {h} is a_partition of X & Pmax is_finer_than Pb \/ {h} & ( for Pmin being a_partition of X st Pmax is_finer_than Pmin holds

for hw being set st hw in Pmin & h c= hw holds

Pb \/ {h} is_finer_than Pmin ) )

A2: {h} c= bool X

let Pmax be a_partition of X; :: thesis: ( ex hy being set st

( hy in Pmax & hy c= h ) & ( for x being set holds

( not x in Pmax or x c= h or h c= x or h misses x ) ) implies for Pb being set st ( for x being set holds

( x in Pb iff ( x in Pmax & x misses h ) ) ) holds

( Pb \/ {h} is a_partition of X & Pmax is_finer_than Pb \/ {h} & ( for Pmin being a_partition of X st Pmax is_finer_than Pmin holds

for hw being set st hw in Pmin & h c= hw holds

Pb \/ {h} is_finer_than Pmin ) ) )

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: for Pb being set st ( for x being set holds

( x in Pb iff ( x in Pmax & x misses h ) ) ) holds

( Pb \/ {h} is a_partition of X & Pmax is_finer_than Pb \/ {h} & ( for Pmin being a_partition of X st Pmax is_finer_than Pmin holds

for hw being set st hw in Pmin & h c= hw holds

Pb \/ {h} is_finer_than Pmin ) )

( x in Pb iff ( x in Pmax & x misses h ) ) ) implies ( Pb \/ {h} is a_partition of X & Pmax is_finer_than Pb \/ {h} & ( for Pmin being a_partition of X st Pmax is_finer_than Pmin holds

for hw being set st hw in Pmin & h c= hw holds

Pb \/ {h} is_finer_than Pmin ) ) )

assume A11: for x being set holds

( x in Pb iff ( x in Pmax & x misses h ) ) ; :: thesis: ( Pb \/ {h} is a_partition of X & Pmax is_finer_than Pb \/ {h} & ( for Pmin being a_partition of X st Pmax is_finer_than Pmin holds

for hw being set st hw in Pmin & h c= hw holds

Pb \/ {h} is_finer_than Pmin ) )

set P = Pb \/ {h};

A12: Pb c= Pb \/ {h} by XBOOLE_1:7;

A13: Pb c= Pmax by A11;

A21: union Pmax = X by EQREL_1:def 4;

A22: X c= union (Pb \/ {h})

then A27: Pb \/ {h} c= bool X by A2, XBOOLE_1:8;

union (Pb \/ {h}) c= X

hence Pb \/ {h} is a_partition of X by A27, A14, EQREL_1:def 4; :: thesis: ( Pmax is_finer_than Pb \/ {h} & ( for Pmin being a_partition of X st Pmax is_finer_than Pmin holds

for hw being set st hw in Pmin & h c= hw holds

Pb \/ {h} is_finer_than Pmin ) )

thus Pmax is_finer_than Pb \/ {h} :: thesis: for Pmin being a_partition of X st Pmax is_finer_than Pmin holds

for hw being set st hw in Pmin & h c= hw holds

Pb \/ {h} is_finer_than Pmin

Pb \/ {h} is_finer_than Pmin )

assume A30: Pmax is_finer_than Pmin ; :: thesis: for hw being set st hw in Pmin & h c= hw holds

Pb \/ {h} is_finer_than Pmin

let hw be set ; :: thesis: ( hw in Pmin & h c= hw implies Pb \/ {h} is_finer_than Pmin )

assume that

A31: hw in Pmin and

A32: h c= hw ; :: thesis: Pb \/ {h} is_finer_than Pmin

let s be set ; :: according to SETFAM_1:def 2 :: thesis: ( not s in Pb \/ {h} or ex b_{1} being set st

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

assume A33: s in Pb \/ {h} ; :: thesis: ex b_{1} being set st

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

( hy in Pmax & hy c= h ) & ( for x being set holds

( not x in Pmax or x c= h or h c= x or h misses x ) ) holds

for Pb being set st ( for x being set holds

( x in Pb iff ( x in Pmax & x misses h ) ) ) holds

( Pb \/ {h} is a_partition of X & Pmax is_finer_than Pb \/ {h} & ( for Pmin being a_partition of X st Pmax is_finer_than Pmin holds

for hw being set st hw in Pmin & h c= hw holds

Pb \/ {h} is_finer_than Pmin ) ) )

assume A1: h c= X ; :: thesis: for Pmax being a_partition of X st ex hy being set st

( hy in Pmax & hy c= h ) & ( for x being set holds

( not x in Pmax or x c= h or h c= x or h misses x ) ) holds

for Pb being set st ( for x being set holds

( x in Pb iff ( x in Pmax & x misses h ) ) ) holds

( Pb \/ {h} is a_partition of X & Pmax is_finer_than Pb \/ {h} & ( for Pmin being a_partition of X st Pmax is_finer_than Pmin holds

for hw being set st hw in Pmin & h c= hw holds

Pb \/ {h} is_finer_than Pmin ) )

A2: {h} c= bool X

proof

A3:
h in {h}
by TARSKI:def 1;
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in {h} or s in bool X )

assume s in {h} ; :: thesis: s in bool X

then s = h by TARSKI:def 1;

hence s in bool X by A1; :: thesis: verum

end;assume s in {h} ; :: thesis: s in bool X

then s = h by TARSKI:def 1;

hence s in bool X by A1; :: thesis: verum

let Pmax be a_partition of X; :: thesis: ( ex hy being set st

( hy in Pmax & hy c= h ) & ( for x being set holds

( not x in Pmax or x c= h or h c= x or h misses x ) ) implies for Pb being set st ( for x being set holds

( x in Pb iff ( x in Pmax & x misses h ) ) ) holds

( Pb \/ {h} is a_partition of X & Pmax is_finer_than Pb \/ {h} & ( for Pmin being a_partition of X st Pmax is_finer_than Pmin holds

for hw being set st hw in Pmin & h c= hw holds

Pb \/ {h} is_finer_than Pmin ) ) )

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: for Pb being set st ( for x being set holds

( x in Pb iff ( x in Pmax & x misses h ) ) ) holds

( Pb \/ {h} is a_partition of X & Pmax is_finer_than Pb \/ {h} & ( for Pmin being a_partition of X st Pmax is_finer_than Pmin holds

for hw being set st hw in Pmin & h c= hw holds

Pb \/ {h} is_finer_than Pmin ) )

A6: now :: thesis: for s being set st s in Pmax & h c= s holds

h = s

let Pb be set ; :: thesis: ( ( for x being set holds h = s

let s be set ; :: thesis: ( s in Pmax & h c= s implies h = s )

assume that

A7: s in Pmax and

A8: h c= s ; :: thesis: h = s

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

end;assume that

A7: s in Pmax and

A8: h c= s ; :: thesis: h = s

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

( x in Pb iff ( x in Pmax & x misses h ) ) ) implies ( Pb \/ {h} is a_partition of X & Pmax is_finer_than Pb \/ {h} & ( for Pmin being a_partition of X st Pmax is_finer_than Pmin holds

for hw being set st hw in Pmin & h c= hw holds

Pb \/ {h} is_finer_than Pmin ) ) )

assume A11: for x being set holds

( x in Pb iff ( x in Pmax & x misses h ) ) ; :: thesis: ( Pb \/ {h} is a_partition of X & Pmax is_finer_than Pb \/ {h} & ( for Pmin being a_partition of X st Pmax is_finer_than Pmin holds

for hw being set st hw in Pmin & h c= hw holds

Pb \/ {h} is_finer_than Pmin ) )

set P = Pb \/ {h};

A12: Pb c= Pb \/ {h} by XBOOLE_1:7;

A13: Pb c= Pmax by A11;

A14: now :: thesis: for A being Subset of X st A in Pb \/ {h} holds

( A <> {} & ( for B being Subset of X holds

( not B in Pb \/ {h} or A = B or A misses B ) ) )

A20:
{h} c= Pb \/ {h}
by XBOOLE_1:7;( A <> {} & ( for B being Subset of X holds

( not B in Pb \/ {h} or A = B or A misses B ) ) )

let A be Subset of X; :: thesis: ( A in Pb \/ {h} implies ( A <> {} & ( for B being Subset of X holds

( not B in Pb \/ {h} or A = B or A misses B ) ) ) )

assume A15: A in Pb \/ {h} ; :: thesis: ( A <> {} & ( for B being Subset of X holds

( not B in Pb \/ {h} or A = B or A misses B ) ) )

hence A <> {} ; :: thesis: for B being Subset of X holds

( not B in Pb \/ {h} or A = B or A misses B )

thus for B being Subset of X holds

( not B in Pb \/ {h} or A = B or A misses B ) :: thesis: verum

end;( not B in Pb \/ {h} or A = B or A misses B ) ) ) )

assume A15: A in Pb \/ {h} ; :: thesis: ( A <> {} & ( for B being Subset of X holds

( not B in Pb \/ {h} or A = B or A misses B ) ) )

hence A <> {} ; :: thesis: for B being Subset of X holds

( not B in Pb \/ {h} or A = B or A misses B )

thus for B being Subset of X holds

( not B in Pb \/ {h} or A = B or A misses B ) :: thesis: verum

proof

let B be Subset of X; :: thesis: ( not B in Pb \/ {h} or A = B or A misses B )

assume A16: B in Pb \/ {h} ; :: thesis: ( A = B or A misses B )

end;assume A16: B in Pb \/ {h} ; :: thesis: ( A = B or A misses B )

per cases
( A in Pb or A in {h} )
by A15, XBOOLE_0:def 3;

end;

suppose A17:
A in Pb
; :: thesis: ( A = B or A misses B )

end;

A21: union Pmax = X by EQREL_1:def 4;

A22: X c= union (Pb \/ {h})

proof

Pb c= bool X
by A13, XBOOLE_1:1;
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in X or s in union (Pb \/ {h}) )

assume s in X ; :: thesis: s in union (Pb \/ {h})

then consider t being set such that

A23: s in t and

A24: t in Pmax by A21, TARSKI:def 4;

end;assume s in X ; :: thesis: s in union (Pb \/ {h})

then consider t being set such that

A23: s in t and

A24: t in Pmax by A21, TARSKI:def 4;

then A27: Pb \/ {h} c= bool X by A2, XBOOLE_1:8;

union (Pb \/ {h}) c= X

proof

then
union (Pb \/ {h}) = X
by A22, XBOOLE_0:def 10;
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in union (Pb \/ {h}) or s in X )

assume s in union (Pb \/ {h}) ; :: thesis: s in X

then ex t being set st

( s in t & t in Pb \/ {h} ) by TARSKI:def 4;

hence s in X by A27; :: thesis: verum

end;assume s in union (Pb \/ {h}) ; :: thesis: s in X

then ex t being set st

( s in t & t in Pb \/ {h} ) by TARSKI:def 4;

hence s in X by A27; :: thesis: verum

hence Pb \/ {h} is a_partition of X by A27, A14, EQREL_1:def 4; :: thesis: ( Pmax is_finer_than Pb \/ {h} & ( for Pmin being a_partition of X st Pmax is_finer_than Pmin holds

for hw being set st hw in Pmin & h c= hw holds

Pb \/ {h} is_finer_than Pmin ) )

thus Pmax is_finer_than Pb \/ {h} :: thesis: for Pmin being a_partition of X st Pmax is_finer_than Pmin holds

for hw being set st hw in Pmin & h c= hw holds

Pb \/ {h} is_finer_than Pmin

proof

let Pmin be a_partition of X; :: thesis: ( Pmax is_finer_than Pmin implies for hw being set st hw in Pmin & h c= hw holds
let x be set ; :: according to SETFAM_1:def 2 :: thesis: ( not x in Pmax or ex b_{1} being set st

( b_{1} in Pb \/ {h} & x c= b_{1} ) )

assume A28: x in Pmax ; :: thesis: ex b_{1} being set st

( b_{1} in Pb \/ {h} & x c= b_{1} )

end;( b

assume A28: x in Pmax ; :: thesis: ex b

( b

per cases
( x c= h or not x c= h )
;

end;

suppose A29:
not x c= h
; :: thesis: ex b_{1} being set st

( b_{1} in Pb \/ {h} & x c= b_{1} )

( b

end;

Pb \/ {h} is_finer_than Pmin )

assume A30: Pmax is_finer_than Pmin ; :: thesis: for hw being set st hw in Pmin & h c= hw holds

Pb \/ {h} is_finer_than Pmin

let hw be set ; :: thesis: ( hw in Pmin & h c= hw implies Pb \/ {h} is_finer_than Pmin )

assume that

A31: hw in Pmin and

A32: h c= hw ; :: thesis: Pb \/ {h} is_finer_than Pmin

let s be set ; :: according to SETFAM_1:def 2 :: thesis: ( not s in Pb \/ {h} or ex b

( b

assume A33: s in Pb \/ {h} ; :: thesis: ex b

( b

per cases
( s in Pb or s in {h} )
by A33, XBOOLE_0:def 3;

end;

suppose
s in Pb
; :: thesis: ex b_{1} being set st

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

( b

then
s in Pmax
by A11;

hence ex b_{1} being set st

( b_{1} in Pmin & s c= b_{1} )
by A30; :: thesis: verum

end;hence ex b

( b

suppose
s in {h}
; :: thesis: ex b_{1} being set st

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

( b

then
s = h
by TARSKI:def 1;

hence ex b_{1} being set st

( b_{1} in Pmin & s c= b_{1} )
by A31, A32; :: thesis: verum

end;hence ex b

( b