:: deftheorem Def7 defines Closed_Domains_Meet TDLAT_1:def 7 :
for T being TopSpace
for b2 being BinOp of (Closed_Domains_of T) holds
( b2 = Closed_Domains_Meet T iff for A, B being Element of Closed_Domains_of T holds b2 . (A,B) = Cl (Int (A /\ B)) );