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 = [#] (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 )
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 = [#] (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 )
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 = [#] (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 )
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 = [#] (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 )
let A be set ; :: thesis: ( A in product_prebasis J & (proj (J,i)) " {xi} c= A & not A = [#] (product J) 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 = [#] (product J) 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 = [#] (product J) 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 = [#] (product J) ; :: 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 A2, Th10;
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