let I be non empty set ; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of
for i being Element of I
for xi being Element of (J . i)
for G being Subset of (product_prebasis J) st (proj J,i) " {xi} c= union G & ( for A being set st A in product_prebasis J & A in G holds
not (proj J,i) " {xi} c= A ) holds
[#] (product J) c= union G
let J be non-Empty TopSpace-yielding ManySortedSet of ; :: thesis: for i being Element of I
for xi being Element of (J . i)
for G being Subset of (product_prebasis J) st (proj J,i) " {xi} c= union G & ( for A being set st A in product_prebasis J & A in G holds
not (proj J,i) " {xi} c= A ) holds
[#] (product J) c= union G
let i be Element of I; :: thesis: for xi being Element of (J . i)
for G being Subset of (product_prebasis J) st (proj J,i) " {xi} c= union G & ( for A being set st A in product_prebasis J & A in G holds
not (proj J,i) " {xi} c= A ) holds
[#] (product J) c= union G
let xi be Element of (J . i); :: thesis: for G being Subset of (product_prebasis J) st (proj J,i) " {xi} c= union G & ( for A being set st A in product_prebasis J & A in G holds
not (proj J,i) " {xi} c= A ) holds
[#] (product J) c= union G
let G be Subset of (product_prebasis J); :: thesis: ( (proj J,i) " {xi} c= union G & ( for A being set st A in product_prebasis J & A in G holds
not (proj J,i) " {xi} c= A ) implies [#] (product J) c= union G )
assume that
A1: (proj J,i) " {xi} c= union G and
A2: for A being set st A in product_prebasis J & A in G holds
not (proj J,i) " {xi} c= A ; :: thesis: [#] (product J) c= union G
let f be set ; :: according to TARSKI:def 3 :: thesis: ( not f in [#] (product J) or f in union G )
assume f in [#] (product J) ; :: thesis: f in union G
then reconsider f' = f as Element of (product J) ;
set g = f' +* i,xi;
A3: f' +* i,xi in (proj J,i) " {xi} by Th11;
then consider Ag being set such that
A4: f' +* i,xi in Ag and
A5: Ag in G by A1, TARSKI:def 4;
consider i2 being Element of I, Ai2 being Subset of (J . i2) such that
Ai2 is open and
A6: (proj J,i2) " Ai2 = Ag by A5, Th17;
A7: not (proj J,i) " {xi} c= (proj J,i2) " Ai2 by A2, A5, A6;
A8: Ai2 <> [#] (J . i2)

proof

assume Ai2 = [#] (J . i2) ; :: thesis: contradiction
then (proj J,i2) " Ai2 = [#] (product J) by Th10
.= the carrier of (product J) ;
hence contradiction by A2, A5, A6; :: thesis: verum

end;

i <> i2

proof

assume A9: i = i2 ; :: thesis: contradiction
then A10: not xi in Ai2 by A7, A8, Th12;
reconsider Ai2' = Ai2 as Subset of (J . i) by A9;
((proj J,i) " {xi}) /\ ((proj J,i) " Ai2') <> {} by A3, A4, A6, A9, XBOOLE_0:def 4;
then (proj J,i) " {xi} meets (proj J,i) " Ai2' by XBOOLE_0:def 7;
hence contradiction by A10, Th9; :: thesis: verum

end;

then f in (proj J,i2) " Ai2 by A4, A6, Th13;
hence f in union G by A5, A6, TARSKI:def 4; :: thesis: verum