let L be GAD_Lattice; ( ( for a, b being Element of L holds (a "\/" b) "/\" b = b ) implies for a, b, c being Element of L holds (a "\/" b) "/\" c = (b "\/" a) "/\" c )
assume AA:
for a, b being Element of L holds (a "\/" b) "/\" b = b
; for a, b, c being Element of L holds (a "\/" b) "/\" c = (b "\/" a) "/\" c
let a, b, c be Element of L; (a "\/" b) "/\" c = (b "\/" a) "/\" c
aa:
(b "\/" a) "/\" a = a
by AA;
S1:
ex d being Element of L st
( (a "\/" b) "/\" c [= d & (b "\/" a) "/\" c [= d )
((a "\/" b) "/\" c) "\/" ((b "\/" a) "/\" c) = ((b "\/" a) "/\" c) "\/" ((a "\/" b) "/\" c)
by S1, DefB2;
then
((a "\/" b) "/\" c) "/\" ((b "\/" a) "/\" c) = ((b "\/" a) "/\" c) "/\" ((a "\/" b) "/\" c)
by IffComm;
then
(a "\/" b) "/\" (c "/\" ((b "\/" a) "/\" c)) = ((b "\/" a) "/\" c) "/\" ((a "\/" b) "/\" c)
by LATTICES:def 7;
then
(a "\/" b) "/\" (c "/\" ((b "\/" a) "/\" c)) = (b "\/" a) "/\" (c "/\" ((a "\/" b) "/\" c))
by LATTICES:def 7;
then
(a "\/" b) "/\" ((b "\/" a) "/\" c) = (b "\/" a) "/\" (c "/\" ((a "\/" b) "/\" c))
by Lem36c;
then
(a "\/" b) "/\" ((b "\/" a) "/\" c) = (b "\/" a) "/\" ((a "\/" b) "/\" c)
by Lem36c;
then
(a "\/" b) "/\" (((b "\/" a) "/\" c) "/\" c) = ((b "\/" a) "/\" ((a "\/" b) "/\" c)) "/\" c
by LATTICES:def 7;
then
(a "\/" b) "/\" ((b "\/" a) "/\" (c "/\" c)) = ((b "\/" a) "/\" ((a "\/" b) "/\" c)) "/\" c
by LATTICES:def 7;
then
(a "\/" b) "/\" ((b "\/" a) "/\" c) = ((b "\/" a) "/\" ((a "\/" b) "/\" c)) "/\" c
by IMeet;
then
(a "\/" b) "/\" ((b "\/" a) "/\" c) = (b "\/" a) "/\" (((a "\/" b) "/\" c) "/\" c)
by LATTICES:def 7;
then
(a "\/" b) "/\" ((b "\/" a) "/\" c) = (b "\/" a) "/\" ((a "\/" b) "/\" (c "/\" c))
by LATTICES:def 7;
then
(a "\/" b) "/\" ((b "\/" a) "/\" c) = (b "\/" a) "/\" ((a "\/" b) "/\" c)
by IMeet;
then
((a "\/" b) "/\" (b "\/" a)) "/\" c = (b "\/" a) "/\" ((a "\/" b) "/\" c)
by LATTICES:def 7;
then
((a "\/" b) "/\" (b "\/" a)) "/\" c = ((b "\/" a) "/\" (a "\/" b)) "/\" c
by LATTICES:def 7;
then
(((a "\/" b) "/\" b) "\/" ((a "\/" b) "/\" a)) "/\" c = ((b "\/" a) "/\" (a "\/" b)) "/\" c
by LATTICES:def 11;
then
(b "\/" ((a "\/" b) "/\" a)) "/\" c = ((b "\/" a) "/\" (a "\/" b)) "/\" c
by AA;
then
(b "\/" a) "/\" c = ((b "\/" a) "/\" (a "\/" b)) "/\" c
by DefA2;
then
(b "\/" a) "/\" c = (((b "\/" a) "/\" a) "\/" ((b "\/" a) "/\" b)) "/\" c
by LATTICES:def 11;
hence
(a "\/" b) "/\" c = (b "\/" a) "/\" c
by DefA2, aa; verum