let I be non empty set ; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of
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 TopSpace-yielding ManySortedSet of ; :: 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 A1: 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 ) )
assume A2: (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 A3: 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 )
consider i1 being Element of I, Ai1 being Subset of (J . i1) such that
A4: Ai1 is open and
A5: (proj J,i1) " Ai1 = A by A1, Th17;
A6: Ai1 <> [#] (J . i1) by A3, A5, Th10;
then A7: J . i = J . i1 by A2, A5, Th12;
reconsider Ai = Ai1 as Subset of (J . i) by A2, A5, A6, Th12;
take Ai ; :: thesis: ( Ai <> [#] (J . i) & xi in Ai & Ai is open & A = (proj J,i) " Ai )
thus Ai <> [#] (J . i) by A2, A5, A6, Th12; :: thesis: ( xi in Ai & Ai is open & A = (proj J,i) " Ai )
thus xi in Ai by A2, A5, A6, Th12; :: thesis: ( Ai is open & A = (proj J,i) " Ai )
thus Ai is open by A4, A7; :: thesis: A = (proj J,i) " Ai
thus A = (proj J,i) " Ai by A2, A5, A6, Th12; :: thesis: verum