let a, b be Element of dL; 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; verum