theorem :: TOPS_5:61

for I being non empty set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for P being Subset of (product (Carrier J)) holds
( P in FinMeetCl (product_prebasis J) iff 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 & P = product ((Carrier J) +* (product_basis_selector (J,f))) ) ) by Lm3, CANTOR_1:def 3;