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