let I be non empty set ; :: thesis:
let J be non-Empty TopStruct-yielding ManySortedSet of I; :: thesis:
let i be Element of I; :: thesis:
let xi be Element of (J . i); :: thesis:
let G be Subset of (product_prebasis J); :: thesis:
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:
let f be object ; :: according to TARSKI:def 3 :: thesis:
assume f in [#] (product J) ; :: thesis:
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)

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

end;

A8: not (proj (J,i)) " {xi} c= (proj (J,i2)) " Ai2 by A2, A5, A6;
i <> i2

assume A9: i = i2 ; :: thesis:
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:

end;