:: deftheorem Def10 defines Open_Domains_Union TDLAT_1:def 10 :
for T being TopSpace
for b₂ being BinOp of (Open_Domains_of T) holds
( b₂ = Open_Domains_Union T iff for A, B being Element of Open_Domains_of T holds b₂ . (A,B) = Int (Cl (A \/ B)) );