theorem Th17: :: YELLOW17:17

for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I
for xi being Element of (J . i)
for A being set st A in product_prebasis J & (proj (J,i)) " {xi} c= A & not A = [#] (product J) holds
ex Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & Ai is open & A = (proj (J,i)) " Ai )