:: deftheorem Def2 defines Top_Union OPENLATT:def 2 :
for T being non empty TopSpace
for b₂ being BinOp of (Topology_of T) holds
( b₂ = Top_Union T iff for P, Q being Element of Topology_of T holds b₂ . (P,Q) = P \/ Q );