theorem Th34: :: FILTER_0:34

for L being Lattice
for D1, D2 being non empty Subset of L holds
( <.(D1 \/ D2).) = <.(<.D1.) \/ D2).) & <.(D1 \/ D2).) = <.(D1 \/ <.D2.)).) )