defpred S₁[ Subset of (product (Carrier J))] means ex i being set ex T being TopStruct ex V being Subset of T st
( i in I & V is open & T = J . i & $1 = product ((Carrier J) +* (i,V)) );
thus ex F being Subset-Family of (product (Carrier J)) st
for x being Subset of (product (Carrier J)) holds
( x in F iff S₁[x] ) from SUBSET_1:sch 3(); :: thesis: verum