theorem Th25: :: YELLOW_7:25

for L being LATTICE holds
( L is distributive iff L opp is distributive )