theorem Th44: :: FILTER_2:44

for L being Lattice
for D1, D2 being non empty Subset of L
for D19, D29 being non empty Subset of (L .:) holds
( D1 "\/" D2 = (D1 .:) "/\" (D2 .:) & (D1 .:) "\/" (D2 .:) = D1 "/\" D2 & D19 "\/" D29 = (.: D19) "/\" (.: D29) & (.: D19) "\/" (.: D29) = D19 "/\" D29 )