for T being non empty TopSpace
for x, y being Element of LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #)
for x9, y9 being Element of OpenClosedSet T st x = x9 & y = y9 holds
x "/\" y = x9 /\ y9 by Def3;