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