defpred S_{1}[ set ] means verum;

let I be non empty set ; :: thesis: for J being non-Empty TopStruct-yielding ManySortedSet of I

for i being Element of I

for F being Subset of (product_prebasis J) st ( for i being Element of I holds J . i is compact ) & ( for G being finite Subset of F holds not [#] (product J) c= union G ) holds

ex xi being Element of (J . i) st

for G being finite Subset of F holds not (proj (J,i)) " {xi} c= union G

let J be non-Empty TopStruct-yielding ManySortedSet of I; :: thesis: for i being Element of I

for F being Subset of (product_prebasis J) st ( for i being Element of I holds J . i is compact ) & ( for G being finite Subset of F holds not [#] (product J) c= union G ) holds

ex xi being Element of (J . i) st

for G being finite Subset of F holds not (proj (J,i)) " {xi} c= union G

let i be Element of I; :: thesis: for F being Subset of (product_prebasis J) st ( for i being Element of I holds J . i is compact ) & ( for G being finite Subset of F holds not [#] (product J) c= union G ) holds

ex xi being Element of (J . i) st

for G being finite Subset of F holds not (proj (J,i)) " {xi} c= union G

let F be Subset of (product_prebasis J); :: thesis: ( ( for i being Element of I holds J . i is compact ) & ( for G being finite Subset of F holds not [#] (product J) c= union G ) implies ex xi being Element of (J . i) st

for G being finite Subset of F holds not (proj (J,i)) " {xi} c= union G )

assume that

A1: for i being Element of I holds J . i is compact and

A2: for G being finite Subset of F holds not [#] (product J) c= union G ; :: thesis: ex xi being Element of (J . i) st

for G being finite Subset of F holds not (proj (J,i)) " {xi} c= union G

deffunc H_{1}( set ) -> Element of bool the carrier of (product J) = (proj (J,i)) " $1;

defpred S_{2}[ object , object ] means ex A being set st

( A = $2 & $1 in A & (proj (J,i)) " A in F & ( for V being Subset of (J . i) st V = $2 holds

V is open ) );

assume A3: for xi being Element of (J . i) ex G being finite Subset of F st (proj (J,i)) " {xi} c= union G ; :: thesis: contradiction

A4: for xi being object st xi in the carrier of (J . i) holds

ex Ai being object st

( Ai in bool the carrier of (J . i) & S_{2}[xi,Ai] )

A9: dom h = the carrier of (J . i) and

A10: rng h c= bool the carrier of (J . i) and

A11: for xi being object st xi in the carrier of (J . i) holds

S_{2}[xi,h . xi]
from FUNCT_1:sch 6(A4);

reconsider bGip = rng h as Subset-Family of (J . i) by A10;

reconsider bGip = bGip as Subset-Family of (J . i) ;

A12: [#] (J . i) c= union bGip

P is open

J . i is compact by A1;

then consider Gip being Subset-Family of (J . i) such that

A17: Gip c= bGip and

A18: [#] (J . i) c= union Gip and

A19: Gip is finite by A12, A16, Th14;

reconsider Gip = Gip as non empty finite Subset-Family of (J . i) by A18, A19, ZFMISC_1:2;

set Gp = { H_{1}(Ai) where Ai is Element of Gip : S_{1}[Ai] } ;

A20: { H_{1}(Ai) where Ai is Element of Gip : S_{1}[Ai] } c= F
_{1}(Ai) where Ai is Element of Gip : S_{1}[Ai] } is finite
from PRE_CIRC:sch 1();

then reconsider Gp = { H_{1}(Ai) where Ai is Element of Gip : S_{1}[Ai] } as finite Subset of F by A20;

[#] (product J) c= union Gp by A18, Th18;

hence contradiction by A2; :: thesis: verum

let I be non empty set ; :: thesis: for J being non-Empty TopStruct-yielding ManySortedSet of I

for i being Element of I

for F being Subset of (product_prebasis J) st ( for i being Element of I holds J . i is compact ) & ( for G being finite Subset of F holds not [#] (product J) c= union G ) holds

ex xi being Element of (J . i) st

for G being finite Subset of F holds not (proj (J,i)) " {xi} c= union G

let J be non-Empty TopStruct-yielding ManySortedSet of I; :: thesis: for i being Element of I

for F being Subset of (product_prebasis J) st ( for i being Element of I holds J . i is compact ) & ( for G being finite Subset of F holds not [#] (product J) c= union G ) holds

ex xi being Element of (J . i) st

for G being finite Subset of F holds not (proj (J,i)) " {xi} c= union G

let i be Element of I; :: thesis: for F being Subset of (product_prebasis J) st ( for i being Element of I holds J . i is compact ) & ( for G being finite Subset of F holds not [#] (product J) c= union G ) holds

ex xi being Element of (J . i) st

for G being finite Subset of F holds not (proj (J,i)) " {xi} c= union G

let F be Subset of (product_prebasis J); :: thesis: ( ( for i being Element of I holds J . i is compact ) & ( for G being finite Subset of F holds not [#] (product J) c= union G ) implies ex xi being Element of (J . i) st

for G being finite Subset of F holds not (proj (J,i)) " {xi} c= union G )

assume that

A1: for i being Element of I holds J . i is compact and

A2: for G being finite Subset of F holds not [#] (product J) c= union G ; :: thesis: ex xi being Element of (J . i) st

for G being finite Subset of F holds not (proj (J,i)) " {xi} c= union G

deffunc H

defpred S

( A = $2 & $1 in A & (proj (J,i)) " A in F & ( for V being Subset of (J . i) st V = $2 holds

V is open ) );

assume A3: for xi being Element of (J . i) ex G being finite Subset of F st (proj (J,i)) " {xi} c= union G ; :: thesis: contradiction

A4: for xi being object st xi in the carrier of (J . i) holds

ex Ai being object st

( Ai in bool the carrier of (J . i) & S

proof

consider h being Function such that
let xi be object ; :: thesis: ( xi in the carrier of (J . i) implies ex Ai being object st

( Ai in bool the carrier of (J . i) & S_{2}[xi,Ai] ) )

assume xi in the carrier of (J . i) ; :: thesis: ex Ai being object st

( Ai in bool the carrier of (J . i) & S_{2}[xi,Ai] )

then reconsider xi9 = xi as Element of (J . i) ;

consider G being finite Subset of F such that

A5: (proj (J,i)) " {xi9} c= union G by A3;

consider Ai being Subset of (J . i) such that

Ai <> [#] (J . i) and

A6: xi in Ai and

A7: (proj (J,i)) " Ai in G and

A8: Ai is open by A2, A5, Th21;

take Ai ; :: thesis: ( Ai in bool the carrier of (J . i) & S_{2}[xi,Ai] )

thus Ai in bool the carrier of (J . i) ; :: thesis: S_{2}[xi,Ai]

take Ai ; :: thesis: ( Ai = Ai & xi in Ai & (proj (J,i)) " Ai in F & ( for V being Subset of (J . i) st V = Ai holds

V is open ) )

thus Ai = Ai ; :: thesis: ( xi in Ai & (proj (J,i)) " Ai in F & ( for V being Subset of (J . i) st V = Ai holds

V is open ) )

thus xi in Ai by A6; :: thesis: ( (proj (J,i)) " Ai in F & ( for V being Subset of (J . i) st V = Ai holds

V is open ) )

thus (proj (J,i)) " Ai in F by A7; :: thesis: for V being Subset of (J . i) st V = Ai holds

V is open

let V be Subset of (J . i); :: thesis: ( V = Ai implies V is open )

assume V = Ai ; :: thesis: V is open

hence V is open by A8; :: thesis: verum

end;( Ai in bool the carrier of (J . i) & S

assume xi in the carrier of (J . i) ; :: thesis: ex Ai being object st

( Ai in bool the carrier of (J . i) & S

then reconsider xi9 = xi as Element of (J . i) ;

consider G being finite Subset of F such that

A5: (proj (J,i)) " {xi9} c= union G by A3;

consider Ai being Subset of (J . i) such that

Ai <> [#] (J . i) and

A6: xi in Ai and

A7: (proj (J,i)) " Ai in G and

A8: Ai is open by A2, A5, Th21;

take Ai ; :: thesis: ( Ai in bool the carrier of (J . i) & S

thus Ai in bool the carrier of (J . i) ; :: thesis: S

take Ai ; :: thesis: ( Ai = Ai & xi in Ai & (proj (J,i)) " Ai in F & ( for V being Subset of (J . i) st V = Ai holds

V is open ) )

thus Ai = Ai ; :: thesis: ( xi in Ai & (proj (J,i)) " Ai in F & ( for V being Subset of (J . i) st V = Ai holds

V is open ) )

thus xi in Ai by A6; :: thesis: ( (proj (J,i)) " Ai in F & ( for V being Subset of (J . i) st V = Ai holds

V is open ) )

thus (proj (J,i)) " Ai in F by A7; :: thesis: for V being Subset of (J . i) st V = Ai holds

V is open

let V be Subset of (J . i); :: thesis: ( V = Ai implies V is open )

assume V = Ai ; :: thesis: V is open

hence V is open by A8; :: thesis: verum

A9: dom h = the carrier of (J . i) and

A10: rng h c= bool the carrier of (J . i) and

A11: for xi being object st xi in the carrier of (J . i) holds

S

reconsider bGip = rng h as Subset-Family of (J . i) by A10;

reconsider bGip = bGip as Subset-Family of (J . i) ;

A12: [#] (J . i) c= union bGip

proof

for P being Subset of (J . i) st P in bGip holds
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [#] (J . i) or x in union bGip )

assume A13: x in [#] (J . i) ; :: thesis: x in union bGip

then S_{2}[x,h . x]
by A11;

then consider A being set such that

A14: ( A = h . x & x in A & (proj (J,i)) " A in F & ( for V being Subset of (J . i) st V = h . x holds

V is open ) ) ;

( x in h . x & h . x in bGip ) by A9, FUNCT_1:def 3, A14, A13;

hence x in union bGip by TARSKI:def 4; :: thesis: verum

end;assume A13: x in [#] (J . i) ; :: thesis: x in union bGip

then S

then consider A being set such that

A14: ( A = h . x & x in A & (proj (J,i)) " A in F & ( for V being Subset of (J . i) st V = h . x holds

V is open ) ) ;

( x in h . x & h . x in bGip ) by A9, FUNCT_1:def 3, A14, A13;

hence x in union bGip by TARSKI:def 4; :: thesis: verum

P is open

proof

then A16:
bGip is open
by TOPS_2:def 1;
let P be Subset of (J . i); :: thesis: ( P in bGip implies P is open )

assume P in bGip ; :: thesis: P is open

then consider x being object such that

A15: ( x in dom h & P = h . x ) by FUNCT_1:def 3;

S_{2}[x,h . x]
by A9, A11, A15;

hence P is open by A15; :: thesis: verum

end;assume P in bGip ; :: thesis: P is open

then consider x being object such that

A15: ( x in dom h & P = h . x ) by FUNCT_1:def 3;

S

hence P is open by A15; :: thesis: verum

J . i is compact by A1;

then consider Gip being Subset-Family of (J . i) such that

A17: Gip c= bGip and

A18: [#] (J . i) c= union Gip and

A19: Gip is finite by A12, A16, Th14;

reconsider Gip = Gip as non empty finite Subset-Family of (J . i) by A18, A19, ZFMISC_1:2;

set Gp = { H

A20: { H

proof

{ H
let A be object ; :: according to TARSKI:def 3 :: thesis: ( not A in { H_{1}(Ai) where Ai is Element of Gip : S_{1}[Ai] } or A in F )

assume A in { H_{1}(Ai) where Ai is Element of Gip : S_{1}[Ai] }
; :: thesis: A in F

then consider Ai being Element of Gip such that

A21: A = (proj (J,i)) " Ai ;

Ai in Gip ;

then consider x being object such that

A22: ( x in dom h & h . x = Ai ) by A17, FUNCT_1:def 3;

S_{2}[x,h . x]
by A9, A11, A22;

hence A in F by A21, A22; :: thesis: verum

end;assume A in { H

then consider Ai being Element of Gip such that

A21: A = (proj (J,i)) " Ai ;

Ai in Gip ;

then consider x being object such that

A22: ( x in dom h & h . x = Ai ) by A17, FUNCT_1:def 3;

S

hence A in F by A21, A22; :: thesis: verum

then reconsider Gp = { H

[#] (product J) c= union Gp by A18, Th18;

hence contradiction by A2; :: thesis: verum