let I be 2 -element set ; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of I
for i, j being Element of I
for P being Subset of (product (Carrier J)) holds
( not i <> j or not P in product_prebasis J or ex V being Subset of (J . i) st
( V is open & P = product ((i,j) --> (V,([#] (J . j)))) ) or ex W being Subset of (J . j) st
( W is open & P = product ((i,j) --> (([#] (J . i)),W)) ) )
let J be non-Empty TopSpace-yielding ManySortedSet of I; :: thesis: for i, j being Element of I
for P being Subset of (product (Carrier J)) holds
( not i <> j or not P in product_prebasis J or ex V being Subset of (J . i) st
( V is open & P = product ((i,j) --> (V,([#] (J . j)))) ) or ex W being Subset of (J . j) st
( W is open & P = product ((i,j) --> (([#] (J . i)),W)) ) )
let i, j be Element of I; :: thesis: for P being Subset of (product (Carrier J)) holds
( not i <> j or not P in product_prebasis J or ex V being Subset of (J . i) st
( V is open & P = product ((i,j) --> (V,([#] (J . j)))) ) or ex W being Subset of (J . j) st
( W is open & P = product ((i,j) --> (([#] (J . i)),W)) ) )
let P be Subset of (product (Carrier J)); :: thesis: ( not i <> j or not P in product_prebasis J or ex V being Subset of (J . i) st
( V is open & P = product ((i,j) --> (V,([#] (J . j)))) ) or ex W being Subset of (J . j) st
( W is open & P = product ((i,j) --> (([#] (J . i)),W)) ) )
assume A1: ( i <> j & P in product_prebasis J ) ; :: thesis: ( ex V being Subset of (J . i) st
( V is open & P = product ((i,j) --> (V,([#] (J . j)))) ) or ex W being Subset of (J . j) st
( W is open & P = product ((i,j) --> (([#] (J . i)),W)) ) )
then consider k being set , T being TopStruct , U being Subset of T such that
A2: ( k in I & U is open & T = J . k & P = product ((Carrier J) +* (k,U)) ) by WAYBEL18:def 2;
k in {i,j} by A1, A2, Th8;

per cases then ( k = i or k = j ) by TARSKI:def 2;

suppose A3: k = i ; :: thesis: ( ex V being Subset of (J . i) st
( V is open & P = product ((i,j) --> (V,([#] (J . j)))) ) or ex W being Subset of (J . j) st
( W is open & P = product ((i,j) --> (([#] (J . i)),W)) ) )

then reconsider V = U as Subset of (J . i) by A2;

now :: thesis: ex V being Subset of (J . i) st
( V is open & P = product ((i,j) --> (V,([#] (J . j)))) )

take V = V; :: thesis: ( V is open & P = product ((i,j) --> (V,([#] (J . j)))) )
thus V is open by A2, A3; :: thesis: P = product ((i,j) --> (V,([#] (J . j))))
(Carrier J) . j = [#] (J . j) by PENCIL_3:7;
hence P = product ((i,j) --> (V,([#] (J . j)))) by A2, A1, A3, Th34; :: thesis: verum

end;

hence ( ex V being Subset of (J . i) st
( V is open & P = product ((i,j) --> (V,([#] (J . j)))) ) or ex W being Subset of (J . j) st
( W is open & P = product ((i,j) --> (([#] (J . i)),W)) ) ) ; :: thesis: verum

end;

suppose A4: k = j ; :: thesis: ( ex V being Subset of (J . i) st
( V is open & P = product ((i,j) --> (V,([#] (J . j)))) ) or ex W being Subset of (J . j) st
( W is open & P = product ((i,j) --> (([#] (J . i)),W)) ) )

then reconsider W = U as Subset of (J . j) by A2;

now :: thesis: ex W being Subset of (J . j) st
( W is open & P = product ((i,j) --> (([#] (J . i)),W)) )

take W = W; :: thesis: ( W is open & P = product ((i,j) --> (([#] (J . i)),W)) )
thus W is open by A2, A4; :: thesis: P = product ((i,j) --> (([#] (J . i)),W))
(Carrier J) . i = [#] (J . i) by PENCIL_3:7;
hence P = product ((i,j) --> (([#] (J . i)),W)) by A2, A1, A4, Th34; :: thesis: verum

end;

hence ( ex V being Subset of (J . i) st
( V is open & P = product ((i,j) --> (V,([#] (J . j)))) ) or ex W being Subset of (J . j) st
( W is open & P = product ((i,j) --> (([#] (J . i)),W)) ) ) ; :: thesis: verum

end;

end;