let TM be metrizable TopSpace; :: thesis:
defpred S₁[ 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:
assume A1: ( TM | A is second-countable & TM | A is finite-ind & ind A <= 0 ) ; :: thesis:
let F be finite Subset-Family of TM; :: thesis:
assume A2: ( F is open & F is Cover of A ) ; :: thesis:
A3: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis:
assume A4: S₁[n] ; :: thesis:
let A be Subset of TM; :: thesis:
assume that
A5: TM | A is second-countable and
A6: A is finite-ind and
A7: ind A <= 0 ; :: thesis:
let F be finite Subset-Family of TM; :: thesis:
assume that
A8: F is open and
A9: F is Cover of A and
A10: card F <= n + 1 ; :: thesis:

per cases by A10, NAT_1:8;

suppose card F <= n ; :: thesis:

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:

end;

suppose A11: card F = n + 1 ; :: thesis:

per cases ;

suppose n = 0 ; :: thesis:

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:
thus ( rng g is open & rng g is Cover of A ) by A8, A9, A12, FUNCOP_1:8; :: thesis:

hereby :: thesis:

let a be set ; :: thesis:
assume A13: a in F ; :: thesis:
then g . a = x by FUNCOP_1:7;
hence g . a c= a by A12, A13, TARSKI:def 1; :: thesis:

end;

let a, b be set ; :: thesis:
assume that
A14: a in F and
A15: ( b in F & a <> b ) ; :: thesis:
x = a by A12, A14, TARSKI:def 1;
hence g . a misses g . b by A12, A15, TARSKI:def 1; :: thesis:

end;

suppose n > 0 ; :: thesis:

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 ;

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

suppose A25: (F \ {x}) \ {y} is Cover of A ; :: thesis:

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

let a be set ; :: thesis:
assume A41: a in F ; :: thesis:

per cases by A36, A41, XBOOLE_0:def 3;

suppose a in (F \ {x}) \ {y} ; :: thesis:

then ( not a in dom ((x,y) --> (({} TM),({} TM))) & g . a c= a ) by A28, A33, XBOOLE_0:3;
hence gh . a c= a by FUNCT_4:11; :: thesis:

end;

suppose a in {x,y} ; :: thesis:

then ( a = x or a = y ) by TARSKI:def 2;
hence gh . a c= a by A39, A40; :: thesis:

end;

let a, b be set ; :: thesis:
assume that
A42: ( a in F & b in F ) and
A43: a <> b ; :: thesis:

per cases by A36, A42, XBOOLE_0:def 3;

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

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:

end;

suppose ( a in {x,y} or b in {x,y} ) ; :: thesis:

then ( gh . a = {} TM or gh . b = {} TM ) by A39, A40, TARSKI:def 2;
hence gh . a misses gh . b ; :: thesis:

end;

suppose A46: (F \ {x}) \ {y} is not Cover of A ; :: thesis:

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

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:
assume that
A81: a in (F \ {x}) \ {y} and
A82: b in {x,y} and
a <> b ; :: thesis:
( (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 a = x \/ y ; :: thesis:
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:

end;

assume gh . a meets gh . b ; :: thesis:
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:

end;

A88: {x,y} c= dom gh by A67, XBOOLE_1:7;
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

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume A91: z in A ; :: thesis:
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 by A94, XBOOLE_0:def 3;

suppose A96: Gx in (F \ {x}) \ {y} ; :: thesis:

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:

end;

suppose Gx in {(x \/ y)} ; :: thesis:

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:

end;

hence rng gh is Cover of A by SETFAM_1:def 11; :: thesis:
A99: ( gV1 c= V1 & gV2 c= V2 ) by XBOOLE_1:17;

hereby :: thesis:

let a be set ; :: thesis:
assume A100: a in F ; :: thesis:

per cases by A70, A100, XBOOLE_0:def 3;

suppose A101: a in (F \ {x}) \ {y} ; :: thesis:

then A102: (g | ((F \ {x}) \ {y})) . a = g . a by A58, FUNCT_1:47;
( not a in dom ((x,y) --> (gV1,gV2)) & g . a c= a ) by A52, A58, A73, A101, XBOOLE_0:3;
hence gh . a c= a by A102, FUNCT_4:11; :: thesis:

end;

suppose a in {x,y} ; :: thesis:

then ( a = x or a = y ) by TARSKI:def 2;
hence gh . a c= a by A63, A78, A77, A99; :: thesis:

end;

let a, b be set ; :: thesis:
assume that
A103: ( a in F & b in F ) and
A104: a <> b ; :: thesis:

per cases by A70, A103, XBOOLE_0:def 3;

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

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:

end;

suppose ( ( a in (F \ {x}) \ {y} & b in {x,y} ) or ( a in {x,y} & b in (F \ {x}) \ {y} ) ) ; :: thesis:

hence gh . a misses gh . b by A79, A104; :: thesis:

end;

suppose A108: ( a in {x,y} & b in {x,y} ) ; :: thesis:

then ( a = x or a = y ) by TARSKI:def 2;
then ( ( a = x & b = y ) or ( a = y & b = x ) ) by A104, A108, TARSKI:def 2;
hence gh . a misses gh . b by A64, A78, A77, A99, XBOOLE_1:64; :: thesis:

end;

A109: S₁[ 0 ]

proof

let A be Subset of TM; :: thesis:
assume that
TM | A is second-countable and
A is finite-ind and
ind A <= 0 ; :: thesis:
let F be finite Subset-Family of TM; :: thesis:
assume that
F is open and
A110: F is Cover of A and
A111: card F <= 0 ; :: thesis:
( 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:
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:

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A109, A3);
then S₁[ 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: