:: deftheorem Def1 defines Int TDLAT_2:def 1 :
for T being TopSpace
for F, b₃ being Subset-Family of T holds
( b₃ = Int F iff for A being Subset of T holds
( A in b₃ iff ex B being Subset of T st
( A = Int B & B in F ) ) );