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