let I be non empty set ; 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 G being finite Subset of F holds not [#] (product J) c= union G ) holds
for xi being Element of (J . i)
for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds
ex Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open )
let J be non-Empty TopStruct-yielding ManySortedSet of I; for i being Element of I
for F being Subset of (product_prebasis J) st ( for G being finite Subset of F holds not [#] (product J) c= union G ) holds
for xi being Element of (J . i)
for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds
ex Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open )
let i be Element of I; for F being Subset of (product_prebasis J) st ( for G being finite Subset of F holds not [#] (product J) c= union G ) holds
for xi being Element of (J . i)
for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds
ex Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open )
let F be Subset of (product_prebasis J); ( ( for G being finite Subset of F holds not [#] (product J) c= union G ) implies for xi being Element of (J . i)
for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds
ex Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open ) )
assume A1:
for G being finite Subset of F holds not [#] (product J) c= union G
; for xi being Element of (J . i)
for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds
ex Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open )
let xi be Element of (J . i); for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds
ex Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open )
let G be finite Subset of F; ( (proj (J,i)) " {xi} c= union G implies ex Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open ) )
assume
(proj (J,i)) " {xi} c= union G
; ex Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open )
then consider A being set such that
A2:
A in product_prebasis J
and
A3:
A in G
and
A4:
(proj (J,i)) " {xi} c= A
by A1, Th20;
A <> [#] (product J)
then consider Ai being Subset of (J . i) such that
A5:
Ai <> [#] (J . i)
and
A6:
xi in Ai
and
A7:
Ai is open
and
A8:
A = (proj (J,i)) " Ai
by A2, A4, Th17;
take
Ai
; ( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open )
thus
Ai <> [#] (J . i)
by A5; ( xi in Ai & (proj (J,i)) " Ai in G & Ai is open )
thus
xi in Ai
by A6; ( (proj (J,i)) " Ai in G & Ai is open )
thus
(proj (J,i)) " Ai in G
by A3, A8; Ai is open
thus
Ai is open
by A7; verum