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:88, TARSKI:def 2;
hence a + b = b + a by Lm9, Lm10; :: thesis: verum