let TM be metrizable TopSpace; :: thesis: for A being Subset of TM st TM | A is second-countable & TM | A is finite-ind & ind A <= 0 holds

for F being finite Subset-Family of TM st F is open & F is Cover of A holds

ex g being Function of F,(bool the carrier of TM) st

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) )

defpred S_{1}[ Nat] means for A being Subset of TM st TM | A is second-countable & A is finite-ind & ind A <= 0 holds

for F being finite Subset-Family of TM st F is open & F is Cover of A & card F <= $1 holds

ex g being Function of F,(bool the carrier of TM) st

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) );

let A be Subset of TM; :: thesis: ( TM | A is second-countable & TM | A is finite-ind & ind A <= 0 implies for F being finite Subset-Family of TM st F is open & F is Cover of A holds

ex g being Function of F,(bool the carrier of TM) st

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) ) )

assume A1: ( TM | A is second-countable & TM | A is finite-ind & ind A <= 0 ) ; :: thesis: for F being finite Subset-Family of TM st F is open & F is Cover of A holds

ex g being Function of F,(bool the carrier of TM) st

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) )

let F be finite Subset-Family of TM; :: thesis: ( F is open & F is Cover of A implies ex g being Function of F,(bool the carrier of TM) st

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) ) )

assume A2: ( F is open & F is Cover of A ) ; :: thesis: ex g being Function of F,(bool the carrier of TM) st

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) )

A3: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[ 0 ]
_{1}[n]
from NAT_1:sch 2(A109, A3);

then S_{1}[ card F]
;

hence ex g being Function of F,(bool the carrier of TM) st

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) ) by A1, A2, TOPDIM_1:18; :: thesis: verum

for F being finite Subset-Family of TM st F is open & F is Cover of A holds

ex g being Function of F,(bool the carrier of TM) st

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) )

defpred S

for F being finite Subset-Family of TM st F is open & F is Cover of A & card F <= $1 holds

ex g being Function of F,(bool the carrier of TM) st

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) );

let A be Subset of TM; :: thesis: ( TM | A is second-countable & TM | A is finite-ind & ind A <= 0 implies for F being finite Subset-Family of TM st F is open & F is Cover of A holds

ex g being Function of F,(bool the carrier of TM) st

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) ) )

assume A1: ( TM | A is second-countable & TM | A is finite-ind & ind A <= 0 ) ; :: thesis: for F being finite Subset-Family of TM st F is open & F is Cover of A holds

ex g being Function of F,(bool the carrier of TM) st

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) )

let F be finite Subset-Family of TM; :: thesis: ( F is open & F is Cover of A implies ex g being Function of F,(bool the carrier of TM) st

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) ) )

assume A2: ( F is open & F is Cover of A ) ; :: thesis: ex g being Function of F,(bool the carrier of TM) st

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) )

A3: for n being Nat st S

S

proof

A109:
S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A4: S_{1}[n]
; :: thesis: S_{1}[n + 1]

let A be Subset of TM; :: thesis: ( TM | A is second-countable & A is finite-ind & ind A <= 0 implies for F being finite Subset-Family of TM st F is open & F is Cover of A & card F <= n + 1 holds

ex g being Function of F,(bool the carrier of TM) st

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) ) )

assume that

A5: TM | A is second-countable and

A6: A is finite-ind and

A7: ind A <= 0 ; :: thesis: for F being finite Subset-Family of TM st F is open & F is Cover of A & card F <= n + 1 holds

ex g being Function of F,(bool the carrier of TM) st

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) )

let F be finite Subset-Family of TM; :: thesis: ( F is open & F is Cover of A & card F <= n + 1 implies ex g being Function of F,(bool the carrier of TM) st

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) ) )

assume that

A8: F is open and

A9: F is Cover of A and

A10: card F <= n + 1 ; :: thesis: ex g being Function of F,(bool the carrier of TM) st

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) )

end;assume A4: S

let A be Subset of TM; :: thesis: ( TM | A is second-countable & A is finite-ind & ind A <= 0 implies for F being finite Subset-Family of TM st F is open & F is Cover of A & card F <= n + 1 holds

ex g being Function of F,(bool the carrier of TM) st

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) ) )

assume that

A5: TM | A is second-countable and

A6: A is finite-ind and

A7: ind A <= 0 ; :: thesis: for F being finite Subset-Family of TM st F is open & F is Cover of A & card F <= n + 1 holds

ex g being Function of F,(bool the carrier of TM) st

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) )

let F be finite Subset-Family of TM; :: thesis: ( F is open & F is Cover of A & card F <= n + 1 implies ex g being Function of F,(bool the carrier of TM) st

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) ) )

assume that

A8: F is open and

A9: F is Cover of A and

A10: card F <= n + 1 ; :: thesis: ex g being Function of F,(bool the carrier of TM) st

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) )

per cases
( card F <= n or card F = n + 1 )
by A10, NAT_1:8;

end;

suppose
card F <= n
; :: thesis: ex g being Function of F,(bool the carrier of TM) st

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) )

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) )

hence
ex g being Function of F,(bool the carrier of TM) st

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) ) by A4, A5, A6, A7, A8, A9; :: thesis: verum

end;( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) ) by A4, A5, A6, A7, A8, A9; :: thesis: verum

suppose A11:
card F = n + 1
; :: thesis: ex g being Function of F,(bool the carrier of TM) st

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) )

end;

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) )

per cases
( n = 0 or n > 0 )
;

end;

suppose
n = 0
; :: thesis: ex g being Function of F,(bool the carrier of TM) st

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) )

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) )

then consider x being object such that

A12: F = {x} by A11, CARD_2:42;

set g = F --> x;

( dom (F --> x) = F & rng (F --> x) = F ) by A12, FUNCOP_1:8, FUNCOP_1:13;

then reconsider g = F --> x as Function of F,(bool the carrier of TM) by FUNCT_2:2;

take g ; :: thesis: ( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) )

thus ( rng g is open & rng g is Cover of A ) by A8, A9, A12, FUNCOP_1:8; :: thesis: ( ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) )

assume that

A14: a in F and

A15: ( b in F & a <> b ) ; :: thesis: g . a misses g . b

x = a by A12, A14, TARSKI:def 1;

hence g . a misses g . b by A12, A15, TARSKI:def 1; :: thesis: verum

end;A12: F = {x} by A11, CARD_2:42;

set g = F --> x;

( dom (F --> x) = F & rng (F --> x) = F ) by A12, FUNCOP_1:8, FUNCOP_1:13;

then reconsider g = F --> x as Function of F,(bool the carrier of TM) by FUNCT_2:2;

take g ; :: thesis: ( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) )

thus ( rng g is open & rng g is Cover of A ) by A8, A9, A12, FUNCOP_1:8; :: thesis: ( ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) )

hereby :: thesis: for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b

let a, b be set ; :: thesis: ( a in F & b in F & a <> b implies g . a misses g . b )g . a misses g . b

let a be set ; :: thesis: ( a in F implies g . a c= a )

assume A13: a in F ; :: thesis: g . a c= a

then g . a = x by FUNCOP_1:7;

hence g . a c= a by A12, A13, TARSKI:def 1; :: thesis: verum

end;assume A13: a in F ; :: thesis: g . a c= a

then g . a = x by FUNCOP_1:7;

hence g . a c= a by A12, A13, TARSKI:def 1; :: thesis: verum

assume that

A14: a in F and

A15: ( b in F & a <> b ) ; :: thesis: g . a misses g . b

x = a by A12, A14, TARSKI:def 1;

hence g . a misses g . b by A12, A15, TARSKI:def 1; :: thesis: verum

suppose
n > 0
; :: thesis: ex g being Function of F,(bool the carrier of TM) st

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) )

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) )

then reconsider n1 = n - 1 as Element of NAT by NAT_1:20;

not F is empty by A11;

then consider x being object such that

A16: x in F ;

A17: card (F \ {x}) = n1 + 1 by A11, A16, STIRL2_1:55;

then not F \ {x} is empty ;

then consider y being object such that

A18: y in F \ {x} ;

y in F by A18, XBOOLE_0:def 5;

then reconsider x = x, y = y as open Subset of TM by A8, A16;

set X = {x};

set xy = x \/ y;

set Y = {y};

set XY = {(x \/ y)};

A19: (F \ {x}) \/ {x} = F by A16, ZFMISC_1:116;

set Fxy = (F \ {x}) \ {y};

A20: card ((F \ {x}) \ {y}) = n1 by A17, A18, STIRL2_1:55;

set FXY = ((F \ {x}) \ {y}) \/ {(x \/ y)};

card {(x \/ y)} = 1 by CARD_1:30;

then A21: card (((F \ {x}) \ {y}) \/ {(x \/ y)}) <= n1 + 1 by A20, CARD_2:43;

F \ {x} is open by A8, TOPS_2:15;

then A22: (F \ {x}) \ {y} is open by TOPS_2:15;

A23: ((F \ {x}) \ {y}) \/ {y} = F \ {x} by A18, ZFMISC_1:116;

for A being Subset of TM st A in {(x \/ y)} holds

A is open by TARSKI:def 1;

then A24: {(x \/ y)} is open ;

end;not F is empty by A11;

then consider x being object such that

A16: x in F ;

A17: card (F \ {x}) = n1 + 1 by A11, A16, STIRL2_1:55;

then not F \ {x} is empty ;

then consider y being object such that

A18: y in F \ {x} ;

y in F by A18, XBOOLE_0:def 5;

then reconsider x = x, y = y as open Subset of TM by A8, A16;

set X = {x};

set xy = x \/ y;

set Y = {y};

set XY = {(x \/ y)};

A19: (F \ {x}) \/ {x} = F by A16, ZFMISC_1:116;

set Fxy = (F \ {x}) \ {y};

A20: card ((F \ {x}) \ {y}) = n1 by A17, A18, STIRL2_1:55;

set FXY = ((F \ {x}) \ {y}) \/ {(x \/ y)};

card {(x \/ y)} = 1 by CARD_1:30;

then A21: card (((F \ {x}) \ {y}) \/ {(x \/ y)}) <= n1 + 1 by A20, CARD_2:43;

F \ {x} is open by A8, TOPS_2:15;

then A22: (F \ {x}) \ {y} is open by TOPS_2:15;

A23: ((F \ {x}) \ {y}) \/ {y} = F \ {x} by A18, ZFMISC_1:116;

for A being Subset of TM st A in {(x \/ y)} holds

A is open by TARSKI:def 1;

then A24: {(x \/ y)} is open ;

per cases
( (F \ {x}) \ {y} is Cover of A or not (F \ {x}) \ {y} is Cover of A )
;

end;

suppose A25:
(F \ {x}) \ {y} is Cover of A
; :: thesis: ex g being Function of F,(bool the carrier of TM) st

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) )

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) )

card ((F \ {x}) \ {y}) <= n1 + 1
by A20, NAT_1:13;

then consider g being Function of ((F \ {x}) \ {y}),(bool the carrier of TM) such that

A26: rng g is open and

A27: rng g is Cover of A and

A28: for a being set st a in (F \ {x}) \ {y} holds

g . a c= a and

A29: for a, b being set st a in (F \ {x}) \ {y} & b in (F \ {x}) \ {y} & a <> b holds

g . a misses g . b by A4, A5, A6, A7, A22, A25;

A30: A c= union (rng g) by A27, SETFAM_1:def 11;

set h = (x,y) --> (({} TM),({} TM));

A31: dom ((x,y) --> (({} TM),({} TM))) = {x,y} by FUNCT_4:62;

not x in F \ {x} by ZFMISC_1:56;

then A32: not x in (F \ {x}) \ {y} by ZFMISC_1:56;

not y in (F \ {x}) \ {y} by ZFMISC_1:56;

then A33: (F \ {x}) \ {y} misses {x,y} by A32, ZFMISC_1:51;

A34: x <> y by A18, ZFMISC_1:56;

then A35: rng ((x,y) --> (({} TM),({} TM))) = {({} TM),({} TM)} by FUNCT_4:64;

A36: ((F \ {x}) \ {y}) \/ {x,y} = ((F \ {x}) \ {y}) \/ ({y} \/ {x}) by ENUMSET1:1

.= (((F \ {x}) \ {y}) \/ {y}) \/ {x} by XBOOLE_1:4

.= F by A18, A19, ZFMISC_1:116 ;

A37: dom g = (F \ {x}) \ {y} by FUNCT_2:def 1;

then A38: rng (g +* ((x,y) --> (({} TM),({} TM)))) = (rng g) \/ (rng ((x,y) --> (({} TM),({} TM)))) by A31, A33, NECKLACE:6;

dom (g +* ((x,y) --> (({} TM),({} TM)))) = ((F \ {x}) \ {y}) \/ {x,y} by A31, A37, FUNCT_4:def 1;

then reconsider gh = g +* ((x,y) --> (({} TM),({} TM))) as Function of F,(bool the carrier of TM) by A36, A38, FUNCT_2:2;

take gh ; :: thesis: ( rng gh is open & rng gh is Cover of A & ( for a being set st a in F holds

gh . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

gh . a misses gh . b ) )

( ((x,y) --> (({} TM),({} TM))) . y = {} TM & y in {x,y} ) by FUNCT_4:63, TARSKI:def 2;

then A39: gh . y = {} TM by A31, FUNCT_4:13;

for A being Subset of TM st A in {({} TM),({} TM)} holds

A is open by TARSKI:def 2;

then {({} TM),({} TM)} is open ;

hence rng gh is open by A26, A35, A38, TOPS_2:13; :: thesis: ( rng gh is Cover of A & ( for a being set st a in F holds

gh . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

gh . a misses gh . b ) )

union (rng gh) = (union (rng g)) \/ (union (rng ((x,y) --> (({} TM),({} TM))))) by A38, ZFMISC_1:78

.= (union (rng g)) \/ (union {({} TM)}) by A35, ENUMSET1:29

.= (union (rng g)) \/ ({} TM) by ZFMISC_1:25

.= union (rng g) ;

hence rng gh is Cover of A by A30, SETFAM_1:def 11; :: thesis: ( ( for a being set st a in F holds

gh . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

gh . a misses gh . b ) )

( x in {x,y} & ((x,y) --> (({} TM),({} TM))) . x = {} TM ) by A34, FUNCT_4:63, TARSKI:def 2;

then A40: gh . x = {} TM by A31, FUNCT_4:13;

assume that

A42: ( a in F & b in F ) and

A43: a <> b ; :: thesis: gh . a misses gh . b

end;then consider g being Function of ((F \ {x}) \ {y}),(bool the carrier of TM) such that

A26: rng g is open and

A27: rng g is Cover of A and

A28: for a being set st a in (F \ {x}) \ {y} holds

g . a c= a and

A29: for a, b being set st a in (F \ {x}) \ {y} & b in (F \ {x}) \ {y} & a <> b holds

g . a misses g . b by A4, A5, A6, A7, A22, A25;

A30: A c= union (rng g) by A27, SETFAM_1:def 11;

set h = (x,y) --> (({} TM),({} TM));

A31: dom ((x,y) --> (({} TM),({} TM))) = {x,y} by FUNCT_4:62;

not x in F \ {x} by ZFMISC_1:56;

then A32: not x in (F \ {x}) \ {y} by ZFMISC_1:56;

not y in (F \ {x}) \ {y} by ZFMISC_1:56;

then A33: (F \ {x}) \ {y} misses {x,y} by A32, ZFMISC_1:51;

A34: x <> y by A18, ZFMISC_1:56;

then A35: rng ((x,y) --> (({} TM),({} TM))) = {({} TM),({} TM)} by FUNCT_4:64;

A36: ((F \ {x}) \ {y}) \/ {x,y} = ((F \ {x}) \ {y}) \/ ({y} \/ {x}) by ENUMSET1:1

.= (((F \ {x}) \ {y}) \/ {y}) \/ {x} by XBOOLE_1:4

.= F by A18, A19, ZFMISC_1:116 ;

A37: dom g = (F \ {x}) \ {y} by FUNCT_2:def 1;

then A38: rng (g +* ((x,y) --> (({} TM),({} TM)))) = (rng g) \/ (rng ((x,y) --> (({} TM),({} TM)))) by A31, A33, NECKLACE:6;

dom (g +* ((x,y) --> (({} TM),({} TM)))) = ((F \ {x}) \ {y}) \/ {x,y} by A31, A37, FUNCT_4:def 1;

then reconsider gh = g +* ((x,y) --> (({} TM),({} TM))) as Function of F,(bool the carrier of TM) by A36, A38, FUNCT_2:2;

take gh ; :: thesis: ( rng gh is open & rng gh is Cover of A & ( for a being set st a in F holds

gh . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

gh . a misses gh . b ) )

( ((x,y) --> (({} TM),({} TM))) . y = {} TM & y in {x,y} ) by FUNCT_4:63, TARSKI:def 2;

then A39: gh . y = {} TM by A31, FUNCT_4:13;

for A being Subset of TM st A in {({} TM),({} TM)} holds

A is open by TARSKI:def 2;

then {({} TM),({} TM)} is open ;

hence rng gh is open by A26, A35, A38, TOPS_2:13; :: thesis: ( rng gh is Cover of A & ( for a being set st a in F holds

gh . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

gh . a misses gh . b ) )

union (rng gh) = (union (rng g)) \/ (union (rng ((x,y) --> (({} TM),({} TM))))) by A38, ZFMISC_1:78

.= (union (rng g)) \/ (union {({} TM)}) by A35, ENUMSET1:29

.= (union (rng g)) \/ ({} TM) by ZFMISC_1:25

.= union (rng g) ;

hence rng gh is Cover of A by A30, SETFAM_1:def 11; :: thesis: ( ( for a being set st a in F holds

gh . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

gh . a misses gh . b ) )

( x in {x,y} & ((x,y) --> (({} TM),({} TM))) . x = {} TM ) by A34, FUNCT_4:63, TARSKI:def 2;

then A40: gh . x = {} TM by A31, FUNCT_4:13;

hereby :: thesis: for a, b being set st a in F & b in F & a <> b holds

gh . a misses gh . b

let a, b be set ; :: thesis: ( a in F & b in F & a <> b implies gh . a misses gh . b )gh . a misses gh . b

let a be set ; :: thesis: ( a in F implies gh . b_{1} c= b_{1} )

assume A41: a in F ; :: thesis: gh . b_{1} c= b_{1}

end;assume A41: a in F ; :: thesis: gh . b

assume that

A42: ( a in F & b in F ) and

A43: a <> b ; :: thesis: gh . a misses gh . b

per cases
( ( a in (F \ {x}) \ {y} & b in (F \ {x}) \ {y} ) or a in {x,y} or b in {x,y} )
by A36, A42, XBOOLE_0:def 3;

end;

suppose A44:
( a in (F \ {x}) \ {y} & b in (F \ {x}) \ {y} )
; :: thesis: gh . a misses gh . b

then
not a in dom ((x,y) --> (({} TM),({} TM)))
by A33, XBOOLE_0:3;

then A45: gh . a = g . a by FUNCT_4:11;

( not b in dom ((x,y) --> (({} TM),({} TM))) & g . a misses g . b ) by A29, A33, A43, A44, XBOOLE_0:3;

hence gh . a misses gh . b by A45, FUNCT_4:11; :: thesis: verum

end;then A45: gh . a = g . a by FUNCT_4:11;

( not b in dom ((x,y) --> (({} TM),({} TM))) & g . a misses g . b ) by A29, A33, A43, A44, XBOOLE_0:3;

hence gh . a misses gh . b by A45, FUNCT_4:11; :: thesis: verum

suppose A46:
(F \ {x}) \ {y} is not Cover of A
; :: thesis: ex g being Function of F,(bool the carrier of TM) st

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) )

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) )

A47: (union ((F \ {x}) \ {y})) \/ (x \/ y) =
(union ((F \ {x}) \ {y})) \/ (union {(x \/ y)})
by ZFMISC_1:25

.= union (((F \ {x}) \ {y}) \/ {(x \/ y)}) by ZFMISC_1:78 ;

A48: ((F \ {x}) \ {y}) \/ {(x \/ y)} is open by A22, A24, TOPS_2:13;

A49: union F = (union (F \ {x})) \/ (union {x}) by A19, ZFMISC_1:78

.= (union (F \ {x})) \/ x by ZFMISC_1:25

.= ((union ((F \ {x}) \ {y})) \/ (union {y})) \/ x by A23, ZFMISC_1:78

.= ((union ((F \ {x}) \ {y})) \/ y) \/ x by ZFMISC_1:25

.= (union ((F \ {x}) \ {y})) \/ (y \/ x) by XBOOLE_1:4 ;

A c= union F by A9, SETFAM_1:def 11;

then ((F \ {x}) \ {y}) \/ {(x \/ y)} is Cover of A by A47, A49, SETFAM_1:def 11;

then consider g being Function of (((F \ {x}) \ {y}) \/ {(x \/ y)}),(bool the carrier of TM) such that

A50: rng g is open and

A51: rng g is Cover of A and

A52: for a being set st a in ((F \ {x}) \ {y}) \/ {(x \/ y)} holds

g . a c= a and

A53: for a, b being set st a in ((F \ {x}) \ {y}) \/ {(x \/ y)} & b in ((F \ {x}) \ {y}) \/ {(x \/ y)} & a <> b holds

g . a misses g . b by A4, A5, A6, A7, A21, A48;

A54: rng (g | ((F \ {x}) \ {y})) is open by A50, RELAT_1:70, TOPS_2:11;

x \/ y in {(x \/ y)} by TARSKI:def 1;

then A55: x \/ y in ((F \ {x}) \ {y}) \/ {(x \/ y)} by XBOOLE_0:def 3;

then A56: g . (x \/ y) c= x \/ y by A52;

A57: dom g = ((F \ {x}) \ {y}) \/ {(x \/ y)} by FUNCT_2:def 1;

then A58: dom (g | ((F \ {x}) \ {y})) = (((F \ {x}) \ {y}) \/ {(x \/ y)}) /\ ((F \ {x}) \ {y}) by RELAT_1:61

.= (F \ {x}) \ {y} by XBOOLE_1:21 ;

g . (x \/ y) in rng g by A55, A57, FUNCT_1:def 3;

then reconsider gxy = g . (x \/ y) as open Subset of TM by A50;

set gxyA = gxy /\ A;

gxy /\ A c= gxy by XBOOLE_1:17;

then A59: gxy /\ A c= x \/ y by A56;

[#] (TM | A) = A by PRE_TOPC:def 5;

then reconsider GxyA = gxy /\ A as Subset of (TM | A) by XBOOLE_1:17;

A60: (TM | A) | GxyA = TM | (gxy /\ A) by METRIZTS:9;

TM | A is finite-ind by A6;

then A61: gxy /\ A is finite-ind by A60, TOPDIM_1:18;

then A62: ind (gxy /\ A) = ind (TM | (gxy /\ A)) by TOPDIM_1:17;

ind GxyA <= ind (TM | A) by A6, TOPDIM_1:19;

then ind GxyA <= 0 by A6, A7, TOPDIM_1:17;

then ind (gxy /\ A) <= 0 by A61, TOPDIM_1:21;

then consider V1, V2 being open Subset of TM such that

A63: ( V1 c= x & V2 c= y ) and

A64: V1 misses V2 and

A65: gxy /\ A c= V1 \/ V2 by A5, A59, A60, A61, A62, Lm10;

reconsider gV1 = gxy /\ V1, gV2 = gxy /\ V2 as open Subset of TM ;

set h = (x,y) --> (gV1,gV2);

A66: dom ((x,y) --> (gV1,gV2)) = {x,y} by FUNCT_4:62;

then A67: dom ((g | ((F \ {x}) \ {y})) +* ((x,y) --> (gV1,gV2))) = ((F \ {x}) \ {y}) \/ {x,y} by A58, FUNCT_4:def 1;

not x in F \ {x} by ZFMISC_1:56;

then A68: not x in (F \ {x}) \ {y} by ZFMISC_1:56;

A69: x in {x,y} by TARSKI:def 2;

A70: ((F \ {x}) \ {y}) \/ {x,y} = ((F \ {x}) \ {y}) \/ ({y} \/ {x}) by ENUMSET1:1

.= (((F \ {x}) \ {y}) \/ {y}) \/ {x} by XBOOLE_1:4

.= F by A18, A19, ZFMISC_1:116 ;

for A being Subset of TM st A in {gV1,gV2} holds

A is open by TARSKI:def 2;

then A71: {gV1,gV2} is open ;

A72: y in {x,y} by TARSKI:def 2;

not y in (F \ {x}) \ {y} by ZFMISC_1:56;

then A73: (F \ {x}) \ {y} misses {x,y} by A68, ZFMISC_1:51;

then A74: rng ((g | ((F \ {x}) \ {y})) +* ((x,y) --> (gV1,gV2))) = (rng (g | ((F \ {x}) \ {y}))) \/ (rng ((x,y) --> (gV1,gV2))) by A58, A66, NECKLACE:6;

then reconsider gh = (g | ((F \ {x}) \ {y})) +* ((x,y) --> (gV1,gV2)) as Function of F,(bool the carrier of TM) by A67, A70, FUNCT_2:2;

A75: (F \ {x}) \ {y} c= dom gh by A67, XBOOLE_1:7;

take gh ; :: thesis: ( rng gh is open & rng gh is Cover of A & ( for a being set st a in F holds

gh . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

gh . a misses gh . b ) )

A76: x <> y by A18, ZFMISC_1:56;

then rng ((x,y) --> (gV1,gV2)) = {gV1,gV2} by FUNCT_4:64;

hence rng gh is open by A54, A71, A74, TOPS_2:13; :: thesis: ( rng gh is Cover of A & ( for a being set st a in F holds

gh . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

gh . a misses gh . b ) )

((x,y) --> (gV1,gV2)) . x = gV1 by A76, FUNCT_4:63;

then A77: gh . x = gV1 by A66, A69, FUNCT_4:13;

((x,y) --> (gV1,gV2)) . y = gV2 by FUNCT_4:63;

then A78: gh . y = gV2 by A66, A72, FUNCT_4:13;

A79: for a, b being set st a in (F \ {x}) \ {y} & b in {x,y} & a <> b holds

gh . a misses gh . b

then A89: gh . y in rng gh by A72, FUNCT_1:def 3;

A90: gh . x in rng gh by A69, A88, FUNCT_1:def 3;

A c= union (rng gh)

gh . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

gh . a misses gh . b ) )

A99: ( gV1 c= V1 & gV2 c= V2 ) by XBOOLE_1:17;

assume that

A103: ( a in F & b in F ) and

A104: a <> b ; :: thesis: gh . a misses gh . b

end;.= union (((F \ {x}) \ {y}) \/ {(x \/ y)}) by ZFMISC_1:78 ;

A48: ((F \ {x}) \ {y}) \/ {(x \/ y)} is open by A22, A24, TOPS_2:13;

A49: union F = (union (F \ {x})) \/ (union {x}) by A19, ZFMISC_1:78

.= (union (F \ {x})) \/ x by ZFMISC_1:25

.= ((union ((F \ {x}) \ {y})) \/ (union {y})) \/ x by A23, ZFMISC_1:78

.= ((union ((F \ {x}) \ {y})) \/ y) \/ x by ZFMISC_1:25

.= (union ((F \ {x}) \ {y})) \/ (y \/ x) by XBOOLE_1:4 ;

A c= union F by A9, SETFAM_1:def 11;

then ((F \ {x}) \ {y}) \/ {(x \/ y)} is Cover of A by A47, A49, SETFAM_1:def 11;

then consider g being Function of (((F \ {x}) \ {y}) \/ {(x \/ y)}),(bool the carrier of TM) such that

A50: rng g is open and

A51: rng g is Cover of A and

A52: for a being set st a in ((F \ {x}) \ {y}) \/ {(x \/ y)} holds

g . a c= a and

A53: for a, b being set st a in ((F \ {x}) \ {y}) \/ {(x \/ y)} & b in ((F \ {x}) \ {y}) \/ {(x \/ y)} & a <> b holds

g . a misses g . b by A4, A5, A6, A7, A21, A48;

A54: rng (g | ((F \ {x}) \ {y})) is open by A50, RELAT_1:70, TOPS_2:11;

x \/ y in {(x \/ y)} by TARSKI:def 1;

then A55: x \/ y in ((F \ {x}) \ {y}) \/ {(x \/ y)} by XBOOLE_0:def 3;

then A56: g . (x \/ y) c= x \/ y by A52;

A57: dom g = ((F \ {x}) \ {y}) \/ {(x \/ y)} by FUNCT_2:def 1;

then A58: dom (g | ((F \ {x}) \ {y})) = (((F \ {x}) \ {y}) \/ {(x \/ y)}) /\ ((F \ {x}) \ {y}) by RELAT_1:61

.= (F \ {x}) \ {y} by XBOOLE_1:21 ;

g . (x \/ y) in rng g by A55, A57, FUNCT_1:def 3;

then reconsider gxy = g . (x \/ y) as open Subset of TM by A50;

set gxyA = gxy /\ A;

gxy /\ A c= gxy by XBOOLE_1:17;

then A59: gxy /\ A c= x \/ y by A56;

[#] (TM | A) = A by PRE_TOPC:def 5;

then reconsider GxyA = gxy /\ A as Subset of (TM | A) by XBOOLE_1:17;

A60: (TM | A) | GxyA = TM | (gxy /\ A) by METRIZTS:9;

TM | A is finite-ind by A6;

then A61: gxy /\ A is finite-ind by A60, TOPDIM_1:18;

then A62: ind (gxy /\ A) = ind (TM | (gxy /\ A)) by TOPDIM_1:17;

ind GxyA <= ind (TM | A) by A6, TOPDIM_1:19;

then ind GxyA <= 0 by A6, A7, TOPDIM_1:17;

then ind (gxy /\ A) <= 0 by A61, TOPDIM_1:21;

then consider V1, V2 being open Subset of TM such that

A63: ( V1 c= x & V2 c= y ) and

A64: V1 misses V2 and

A65: gxy /\ A c= V1 \/ V2 by A5, A59, A60, A61, A62, Lm10;

reconsider gV1 = gxy /\ V1, gV2 = gxy /\ V2 as open Subset of TM ;

set h = (x,y) --> (gV1,gV2);

A66: dom ((x,y) --> (gV1,gV2)) = {x,y} by FUNCT_4:62;

then A67: dom ((g | ((F \ {x}) \ {y})) +* ((x,y) --> (gV1,gV2))) = ((F \ {x}) \ {y}) \/ {x,y} by A58, FUNCT_4:def 1;

not x in F \ {x} by ZFMISC_1:56;

then A68: not x in (F \ {x}) \ {y} by ZFMISC_1:56;

A69: x in {x,y} by TARSKI:def 2;

A70: ((F \ {x}) \ {y}) \/ {x,y} = ((F \ {x}) \ {y}) \/ ({y} \/ {x}) by ENUMSET1:1

.= (((F \ {x}) \ {y}) \/ {y}) \/ {x} by XBOOLE_1:4

.= F by A18, A19, ZFMISC_1:116 ;

for A being Subset of TM st A in {gV1,gV2} holds

A is open by TARSKI:def 2;

then A71: {gV1,gV2} is open ;

A72: y in {x,y} by TARSKI:def 2;

not y in (F \ {x}) \ {y} by ZFMISC_1:56;

then A73: (F \ {x}) \ {y} misses {x,y} by A68, ZFMISC_1:51;

then A74: rng ((g | ((F \ {x}) \ {y})) +* ((x,y) --> (gV1,gV2))) = (rng (g | ((F \ {x}) \ {y}))) \/ (rng ((x,y) --> (gV1,gV2))) by A58, A66, NECKLACE:6;

then reconsider gh = (g | ((F \ {x}) \ {y})) +* ((x,y) --> (gV1,gV2)) as Function of F,(bool the carrier of TM) by A67, A70, FUNCT_2:2;

A75: (F \ {x}) \ {y} c= dom gh by A67, XBOOLE_1:7;

take gh ; :: thesis: ( rng gh is open & rng gh is Cover of A & ( for a being set st a in F holds

gh . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

gh . a misses gh . b ) )

A76: x <> y by A18, ZFMISC_1:56;

then rng ((x,y) --> (gV1,gV2)) = {gV1,gV2} by FUNCT_4:64;

hence rng gh is open by A54, A71, A74, TOPS_2:13; :: thesis: ( rng gh is Cover of A & ( for a being set st a in F holds

gh . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

gh . a misses gh . b ) )

((x,y) --> (gV1,gV2)) . x = gV1 by A76, FUNCT_4:63;

then A77: gh . x = gV1 by A66, A69, FUNCT_4:13;

((x,y) --> (gV1,gV2)) . y = gV2 by FUNCT_4:63;

then A78: gh . y = gV2 by A66, A72, FUNCT_4:13;

A79: for a, b being set st a in (F \ {x}) \ {y} & b in {x,y} & a <> b holds

gh . a misses gh . b

proof

A88:
{x,y} c= dom gh
by A67, XBOOLE_1:7;
x \/ y in {(x \/ y)}
by TARSKI:def 1;

then A80: x \/ y in ((F \ {x}) \ {y}) \/ {(x \/ y)} by XBOOLE_0:def 3;

let a, b be set ; :: thesis: ( a in (F \ {x}) \ {y} & b in {x,y} & a <> b implies gh . a misses gh . b )

assume that

A81: a in (F \ {x}) \ {y} and

A82: b in {x,y} and

a <> b ; :: thesis: gh . a misses gh . b

( (g | ((F \ {x}) \ {y})) . a = g . a & not a in dom ((x,y) --> (gV1,gV2)) ) by A58, A73, A81, FUNCT_1:47, XBOOLE_0:3;

then A83: gh . a = g . a by FUNCT_4:11;

A84: a <> x \/ y

then consider z being object such that

A86: z in gh . a and

A87: z in gh . b by XBOOLE_0:3;

( z in gV1 or z in gV2 ) by A78, A77, A82, A87, TARSKI:def 2;

then z in gxy by XBOOLE_0:def 4;

then g . (x \/ y) meets g . a by A83, A86, XBOOLE_0:3;

hence contradiction by A53, A58, A80, A81, A84; :: thesis: verum

end;then A80: x \/ y in ((F \ {x}) \ {y}) \/ {(x \/ y)} by XBOOLE_0:def 3;

let a, b be set ; :: thesis: ( a in (F \ {x}) \ {y} & b in {x,y} & a <> b implies gh . a misses gh . b )

assume that

A81: a in (F \ {x}) \ {y} and

A82: b in {x,y} and

a <> b ; :: thesis: gh . a misses gh . b

( (g | ((F \ {x}) \ {y})) . a = g . a & not a in dom ((x,y) --> (gV1,gV2)) ) by A58, A73, A81, FUNCT_1:47, XBOOLE_0:3;

then A83: gh . a = g . a by FUNCT_4:11;

A84: a <> x \/ y

proof

assume
gh . a meets gh . b
; :: thesis: contradiction
assume
a = x \/ y
; :: thesis: contradiction

then A85: union F = union ((F \ {x}) \ {y}) by A49, A81, XBOOLE_1:12, ZFMISC_1:74;

not A c= union ((F \ {x}) \ {y}) by A46, SETFAM_1:def 11;

hence contradiction by A9, A85, SETFAM_1:def 11; :: thesis: verum

end;then A85: union F = union ((F \ {x}) \ {y}) by A49, A81, XBOOLE_1:12, ZFMISC_1:74;

not A c= union ((F \ {x}) \ {y}) by A46, SETFAM_1:def 11;

hence contradiction by A9, A85, SETFAM_1:def 11; :: thesis: verum

then consider z being object such that

A86: z in gh . a and

A87: z in gh . b by XBOOLE_0:3;

( z in gV1 or z in gV2 ) by A78, A77, A82, A87, TARSKI:def 2;

then z in gxy by XBOOLE_0:def 4;

then g . (x \/ y) meets g . a by A83, A86, XBOOLE_0:3;

hence contradiction by A53, A58, A80, A81, A84; :: thesis: verum

then A89: gh . y in rng gh by A72, FUNCT_1:def 3;

A90: gh . x in rng gh by A69, A88, FUNCT_1:def 3;

A c= union (rng gh)

proof

hence
rng gh is Cover of A
by SETFAM_1:def 11; :: thesis: ( ( for a being set st a in F holds
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in A or z in union (rng gh) )

assume A91: z in A ; :: thesis: z in union (rng gh)

A c= union (rng g) by A51, SETFAM_1:def 11;

then consider G being set such that

A92: z in G and

A93: G in rng g by A91, TARSKI:def 4;

consider Gx being object such that

A94: Gx in ((F \ {x}) \ {y}) \/ {(x \/ y)} and

A95: g . Gx = G by A57, A93, FUNCT_1:def 3;

end;assume A91: z in A ; :: thesis: z in union (rng gh)

A c= union (rng g) by A51, SETFAM_1:def 11;

then consider G being set such that

A92: z in G and

A93: G in rng g by A91, TARSKI:def 4;

consider Gx being object such that

A94: Gx in ((F \ {x}) \ {y}) \/ {(x \/ y)} and

A95: g . Gx = G by A57, A93, FUNCT_1:def 3;

per cases
( Gx in (F \ {x}) \ {y} or Gx in {(x \/ y)} )
by A94, XBOOLE_0:def 3;

end;

suppose A96:
Gx in (F \ {x}) \ {y}
; :: thesis: z in union (rng gh)

then
( (g | ((F \ {x}) \ {y})) . Gx = G & not Gx in dom ((x,y) --> (gV1,gV2)) )
by A58, A73, A95, FUNCT_1:47, XBOOLE_0:3;

then A97: gh . Gx = G by FUNCT_4:11;

gh . Gx in rng gh by A75, A96, FUNCT_1:def 3;

hence z in union (rng gh) by A92, A97, TARSKI:def 4; :: thesis: verum

end;then A97: gh . Gx = G by FUNCT_4:11;

gh . Gx in rng gh by A75, A96, FUNCT_1:def 3;

hence z in union (rng gh) by A92, A97, TARSKI:def 4; :: thesis: verum

suppose
Gx in {(x \/ y)}
; :: thesis: z in union (rng gh)

then A98:
z in gxy
by A92, A95, TARSKI:def 1;

then z in gxy /\ A by A91, XBOOLE_0:def 4;

then ( z in V1 or z in V2 ) by A65, XBOOLE_0:def 3;

then ( z in gV1 or z in gV2 ) by A98, XBOOLE_0:def 4;

hence z in union (rng gh) by A78, A77, A90, A89, TARSKI:def 4; :: thesis: verum

end;then z in gxy /\ A by A91, XBOOLE_0:def 4;

then ( z in V1 or z in V2 ) by A65, XBOOLE_0:def 3;

then ( z in gV1 or z in gV2 ) by A98, XBOOLE_0:def 4;

hence z in union (rng gh) by A78, A77, A90, A89, TARSKI:def 4; :: thesis: verum

gh . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

gh . a misses gh . b ) )

A99: ( gV1 c= V1 & gV2 c= V2 ) by XBOOLE_1:17;

hereby :: thesis: for a, b being set st a in F & b in F & a <> b holds

gh . a misses gh . b

let a, b be set ; :: thesis: ( a in F & b in F & a <> b implies gh . a misses gh . b )gh . a misses gh . b

let a be set ; :: thesis: ( a in F implies gh . b_{1} c= b_{1} )

assume A100: a in F ; :: thesis: gh . b_{1} c= b_{1}

end;assume A100: a in F ; :: thesis: gh . b

per cases
( a in (F \ {x}) \ {y} or a in {x,y} )
by A70, A100, XBOOLE_0:def 3;

end;

assume that

A103: ( a in F & b in F ) and

A104: a <> b ; :: thesis: gh . a misses gh . b

per cases
( ( a in (F \ {x}) \ {y} & b in (F \ {x}) \ {y} ) or ( a in (F \ {x}) \ {y} & b in {x,y} ) or ( a in {x,y} & b in (F \ {x}) \ {y} ) or ( a in {x,y} & b in {x,y} ) )
by A70, A103, XBOOLE_0:def 3;

end;

suppose A105:
( a in (F \ {x}) \ {y} & b in (F \ {x}) \ {y} )
; :: thesis: gh . a misses gh . b

then
( (g | ((F \ {x}) \ {y})) . a = g . a & not a in dom ((x,y) --> (gV1,gV2)) )
by A58, A73, FUNCT_1:47, XBOOLE_0:3;

then A106: gh . a = g . a by FUNCT_4:11;

A107: ( (g | ((F \ {x}) \ {y})) . b = g . b & not b in dom ((x,y) --> (gV1,gV2)) ) by A58, A73, A105, FUNCT_1:47, XBOOLE_0:3;

g . a misses g . b by A53, A58, A104, A105;

hence gh . a misses gh . b by A106, A107, FUNCT_4:11; :: thesis: verum

end;then A106: gh . a = g . a by FUNCT_4:11;

A107: ( (g | ((F \ {x}) \ {y})) . b = g . b & not b in dom ((x,y) --> (gV1,gV2)) ) by A58, A73, A105, FUNCT_1:47, XBOOLE_0:3;

g . a misses g . b by A53, A58, A104, A105;

hence gh . a misses gh . b by A106, A107, FUNCT_4:11; :: thesis: verum

proof

for n being Nat holds S
let A be Subset of TM; :: thesis: ( TM | A is second-countable & A is finite-ind & ind A <= 0 implies for F being finite Subset-Family of TM st F is open & F is Cover of A & card F <= 0 holds

ex g being Function of F,(bool the carrier of TM) st

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) ) )

assume that

TM | A is second-countable and

A is finite-ind and

ind A <= 0 ; :: thesis: for F being finite Subset-Family of TM st F is open & F is Cover of A & card F <= 0 holds

ex g being Function of F,(bool the carrier of TM) st

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) )

let F be finite Subset-Family of TM; :: thesis: ( F is open & F is Cover of A & card F <= 0 implies ex g being Function of F,(bool the carrier of TM) st

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) ) )

assume that

F is open and

A110: F is Cover of A and

A111: card F <= 0 ; :: thesis: ex g being Function of F,(bool the carrier of TM) st

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) )

( rng {} c= bool the carrier of TM & dom {} = F ) by A111;

then reconsider g = {} as Function of F,(bool the carrier of TM) by FUNCT_2:2;

take g ; :: thesis: ( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) )

F = {} by A111;

hence ( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) ) by A110; :: thesis: verum

end;ex g being Function of F,(bool the carrier of TM) st

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) ) )

assume that

TM | A is second-countable and

A is finite-ind and

ind A <= 0 ; :: thesis: for F being finite Subset-Family of TM st F is open & F is Cover of A & card F <= 0 holds

ex g being Function of F,(bool the carrier of TM) st

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) )

let F be finite Subset-Family of TM; :: thesis: ( F is open & F is Cover of A & card F <= 0 implies ex g being Function of F,(bool the carrier of TM) st

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) ) )

assume that

F is open and

A110: F is Cover of A and

A111: card F <= 0 ; :: thesis: ex g being Function of F,(bool the carrier of TM) st

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) )

( rng {} c= bool the carrier of TM & dom {} = F ) by A111;

then reconsider g = {} as Function of F,(bool the carrier of TM) by FUNCT_2:2;

take g ; :: thesis: ( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) )

F = {} by A111;

hence ( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) ) by A110; :: thesis: verum

then S

hence ex g being Function of F,(bool the carrier of TM) st

( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) ) by A1, A2, TOPDIM_1:18; :: thesis: verum