:: deftheorem Def2 defines product_prebasis WAYBEL18:def 2 :
for I being set
for J being TopStruct-yielding ManySortedSet of I
for b₃ being Subset-Family of (product (Carrier J)) holds
( b₃ = product_prebasis J iff for x being Subset of (product (Carrier J)) holds
( x in b₃ iff ex i being set ex T being TopStruct ex V being Subset of T st
( i in I & V is open & T = J . i & x = product ((Carrier J) +* (i,V)) ) ) );