theorem Th62: :: TOPS_5:62

for I being non empty set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for P being non empty Subset of (product (Carrier J)) st P in FinMeetCl (product_prebasis J) holds
ex X being Subset-Family of (product (Carrier J)) ex f being b₁ -valued one-to-one Function st
( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & ( for i being Element of I holds
( (proj (J,i)) .: P is open & ( not i in rng f implies (proj (J,i)) .: P = [#] (J . i) ) ) ) )