theorem Th36: :: FILTER_2:36

for L being Lattice
for D being non empty Subset of L
for D9 being non empty Subset of (L .:) holds
( <.(D .:).) = (.D.> & <.D.) = (.(D .:).> & <.(.: D9).) = (.D9.> & <.D9.) = (.(.: D9).> )