let a be Element of dL; :: thesis: a + (0. dL) = a
( a = In 0 ,2 or a = In 1,2 ) by Lm3, Lm4, CARD_1:88, TARSKI:def 2;
hence a + (0. dL) = a by Lm8, Lm10; :: thesis: verum