:: deftheorem Def3 defines T_meet LOPCLSET:def 3 :
for T being non empty TopSpace
for b₂ being BinOp of (OpenClosedSet T) holds
( b₂ = T_meet T iff for A, B being Element of OpenClosedSet T holds b₂ . (A,B) = A /\ B );