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:50, TARSKI:def 2;
hence a + (0. dL) = a by Lm8, Lm10; :: thesis: verum