:: deftheorem Def3 defines | TOPS_2:def 3 :
for T being TopStruct
for P being Subset of T
for F being Subset-Family of T
for b₄ being Subset-Family of (T | P) holds
( b₄ = F | P iff for Q being Subset of (T | P) holds
( Q in b₄ iff ex R being Subset of T st
( R in F & R /\ P = Q ) ) );