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 Lm2, CARD_1:88, TARSKI:def 2;
hence a + b = b + a by Lm7, Lm8; :: thesis: verum