theorem Th7: :: OPENLATT:7

for T being non empty TopSpace
for p, q being Element of (Open_setLatt T)
for p9, q9 being Element of Topology_of T st p = p9 & q = q9 holds
( p [= q iff p9 c= q9 )