:: deftheorem Def3 defines product WAYBEL18:def 3 :
for I being set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for b₃ being strict TopSpace holds
( b₃ = product J iff ( the carrier of b₃ = product (Carrier J) & product_prebasis J is prebasis of b₃ ) );