theorem Th73: :: FILTER_2:73

for L being Lattice
for P being non empty ClosedSubset of L
for p, q being Element of L
for p9, q9 being Element of (latt (L,P)) st p = p9 & q = q9 holds
( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 )