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 A being set st A in product_prebasis J & (proj (J,i)) " {xi} c= A & not A = [#] () holds
ex Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & Ai is open & A = (proj (J,i)) " Ai )

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 A being set st A in product_prebasis J & (proj (J,i)) " {xi} c= A & not A = [#] () holds
ex Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & Ai is open & A = (proj (J,i)) " Ai )

let i be Element of I; :: thesis: 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 = [#] () holds
ex Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & Ai is open & A = (proj (J,i)) " Ai )

let xi be Element of (J . i); :: thesis: for A being set st A in product_prebasis J & (proj (J,i)) " {xi} c= A & not A = [#] () holds
ex Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & Ai is open & A = (proj (J,i)) " Ai )

let A be set ; :: thesis: ( A in product_prebasis J & (proj (J,i)) " {xi} c= A & not A = [#] () implies ex Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & Ai is open & A = (proj (J,i)) " Ai ) )

assume A in product_prebasis J ; :: thesis: ( not (proj (J,i)) " {xi} c= A or A = [#] () or ex Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & Ai is open & A = (proj (J,i)) " Ai ) )

then consider i1 being Element of I, Ai1 being Subset of (J . i1) such that
A1: Ai1 is open and
A2: (proj (J,i1)) " Ai1 = A by Th16;
assume A3: (proj (J,i)) " {xi} c= A ; :: thesis: ( A = [#] () or ex Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & Ai is open & A = (proj (J,i)) " Ai ) )

assume not A = [#] () ; :: thesis: ex Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & Ai is open & A = (proj (J,i)) " Ai )

then A4: Ai1 <> [#] (J . i1) by ;
then reconsider Ai = Ai1 as Subset of (J . i) by A3, A2, Th12;
take Ai ; :: thesis: ( Ai <> [#] (J . i) & xi in Ai & Ai is open & A = (proj (J,i)) " Ai )
thus Ai <> [#] (J . i) by A3, A2, A4, Th12; :: thesis: ( xi in Ai & Ai is open & A = (proj (J,i)) " Ai )
thus xi in Ai by A3, A2, A4, Th12; :: thesis: ( Ai is open & A = (proj (J,i)) " Ai )
J . i = J . i1 by A3, A2, A4, Th12;
hence Ai is open by A1; :: thesis: A = (proj (J,i)) " Ai
thus A = (proj (J,i)) " Ai by A3, A2, A4, Th12; :: thesis: verum