theorem Th29: :: FILTER_2:29

for L being Lattice
for p being Element of L holds
( (.p.> = <.(p .:).) & (.(p .:).> = <.p.) )