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

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 TopStruct-yielding ManySortedSet of I; :: 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 object ; :: 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 f9 = f as Element of (product J) ;

set g = f9 +* (i,xi);

A3: f9 +* (i,xi) in (proj (J,i)) " {xi} by Th11;

then consider Ag being set such that

A4: f9 +* (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, Th16;

A7: Ai2 <> [#] (J . i2)

i <> i2

hence f in union G by A5, A6, TARSKI:def 4; :: thesis: verum

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 TopStruct-yielding ManySortedSet of I; :: 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 object ; :: 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 f9 = f as Element of (product J) ;

set g = f9 +* (i,xi);

A3: f9 +* (i,xi) in (proj (J,i)) " {xi} by Th11;

then consider Ag being set such that

A4: f9 +* (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, Th16;

A7: Ai2 <> [#] (J . i2)

proof

A8:
not (proj (J,i)) " {xi} c= (proj (J,i2)) " Ai2
by A2, A5, A6;
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;then (proj (J,i2)) " Ai2 = [#] (product J) by Th10

.= the carrier of (product J) ;

hence contradiction by A2, A5, A6; :: thesis: verum

i <> i2

proof

then
f in (proj (J,i2)) " Ai2
by A4, A6, Th13;
assume A9:
i = i2
; :: thesis: contradiction

then reconsider Ai29 = Ai2 as Subset of (J . i) ;

((proj (J,i)) " {xi}) /\ ((proj (J,i)) " Ai29) <> {} by A3, A4, A6, A9, XBOOLE_0:def 4;

then A10: (proj (J,i)) " {xi} meets (proj (J,i)) " Ai29 ;

not xi in Ai2 by A8, A7, A9, Th12;

hence contradiction by A10, Th9; :: thesis: verum

end;then reconsider Ai29 = Ai2 as Subset of (J . i) ;

((proj (J,i)) " {xi}) /\ ((proj (J,i)) " Ai29) <> {} by A3, A4, A6, A9, XBOOLE_0:def 4;

then A10: (proj (J,i)) " {xi} meets (proj (J,i)) " Ai29 ;

not xi in Ai2 by A8, A7, A9, Th12;

hence contradiction by A10, Th9; :: thesis: verum

hence f in union G by A5, A6, TARSKI:def 4; :: thesis: verum