let I be 1 -element set ; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of I
for i being Element of I
for P being Subset of () holds
( P is open iff ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) ) )

let J be non-Empty TopSpace-yielding ManySortedSet of I; :: thesis: for i being Element of I
for P being Subset of () holds
( P is open iff ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) ) )

let i be Element of I; :: thesis: for P being Subset of () holds
( P is open iff ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) ) )

let P be Subset of (); :: thesis: ( P is open iff ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) ) )

hereby :: thesis: ( ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) ) implies P is open )
assume P is open ; :: thesis: ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) )

then P in the topology of () by PRE_TOPC:def 2;
then P in product_prebasis J by Th65;
hence ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) ) by Th64; :: thesis: verum
end;
A1: P is Subset of (product ()) by WAYBEL18:def 3;
assume ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) ) ; :: thesis: P is open
then P in product_prebasis J by ;
then P in the topology of () by Th65;
hence P is open by PRE_TOPC:def 2; :: thesis: verum