defpred S1[ 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 () st ( for i being Element of I holds J . i is compact ) & ( for G being finite Subset of F holds not [#] () 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 () st ( for i being Element of I holds J . i is compact ) & ( for G being finite Subset of F holds not [#] () 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 () st ( for i being Element of I holds J . i is compact ) & ( for G being finite Subset of F holds not [#] () 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 (); :: thesis: ( ( for i being Element of I holds J . i is compact ) & ( for G being finite Subset of F holds not [#] () 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 [#] () 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 H1( set ) -> Element of bool the carrier of () = (proj (J,i)) " \$1;
defpred S2[ 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) & S2[xi,Ai] )
proof
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) & S2[xi,Ai] ) )

assume xi in the carrier of (J . i) ; :: thesis: ex Ai being object st
( Ai in bool the carrier of (J . i) & S2[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) & S2[xi,Ai] )
thus Ai in bool the carrier of (J . i) ; :: thesis: S2[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;
consider h being Function such that
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
S2[xi,h . xi] from 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
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 S2[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 ;
hence x in union bGip by TARSKI:def 4; :: thesis: verum
end;
for P being Subset of (J . i) st P in bGip holds
P is open
proof
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;
S2[x,h . x] by A9, A11, A15;
hence P is open by A15; :: thesis: verum
end;
then A16: bGip is open by TOPS_2:def 1;
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 ;
reconsider Gip = Gip as non empty finite Subset-Family of (J . i) by ;
set Gp = { H1(Ai) where Ai is Element of Gip : S1[Ai] } ;
A20: { H1(Ai) where Ai is Element of Gip : S1[Ai] } c= F
proof
let A be object ; :: according to TARSKI:def 3 :: thesis: ( not A in { H1(Ai) where Ai is Element of Gip : S1[Ai] } or A in F )
assume A in { H1(Ai) where Ai is Element of Gip : S1[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 ;
S2[x,h . x] by A9, A11, A22;
hence A in F by ; :: thesis: verum
end;
{ H1(Ai) where Ai is Element of Gip : S1[Ai] } is finite from then reconsider Gp = { H1(Ai) where Ai is Element of Gip : S1[Ai] } as finite Subset of F by A20;
[#] () c= union Gp by ;
hence contradiction by A2; :: thesis: verum