:: deftheorem Def2 defines Domains_Union TDLAT_1:def 2 :
for T being TopSpace
for b₂ being BinOp of (Domains_of T) holds
( b₂ = Domains_Union T iff for A, B being Element of Domains_of T holds b₂ . (A,B) = (Int (Cl (A \/ B))) \/ (A \/ B) );