let L be GAD_Lattice; ( ( for a, b, c being Element of L holds (a "\/" b) "/\" c = (b "\/" a) "/\" c ) implies for a, b, c being Element of L holds (a "\/" b) "/\" c = (a "/\" c) "\/" (b "/\" c) )
assume A1:
for a, b, c being Element of L holds (a "\/" b) "/\" c = (b "\/" a) "/\" c
; for a, b, c being Element of L holds (a "\/" b) "/\" c = (a "/\" c) "\/" (b "/\" c)
let a, b, c be Element of L; (a "\/" b) "/\" c = (a "/\" c) "\/" (b "/\" c)
(a "/\" c) "\/" (b "/\" c) =
((a "/\" c) "\/" b) "/\" ((a "/\" c) "\/" c)
by DefLDS
.=
((a "/\" c) "\/" b) "/\" c
by LATTICES:def 8
.=
(b "\/" (a "/\" c)) "/\" c
by A1
.=
((b "\/" a) "/\" (b "\/" c)) "/\" c
by DefLDS
.=
(((b "\/" a) "/\" b) "\/" ((b "\/" a) "/\" c)) "/\" c
by LATTICES:def 11
.=
(b "\/" ((b "\/" a) "/\" c)) "/\" c
by DefA2
.=
((b "\/" (b "\/" a)) "/\" (b "\/" c)) "/\" c
by DefLDS
.=
(b "\/" (b "\/" a)) "/\" ((b "\/" c) "/\" c)
by LATTICES:def 7
.=
(b "\/" (b "\/" a)) "/\" ((c "\/" b) "/\" c)
by A1
.=
(b "\/" (b "\/" a)) "/\" c
by DefA2
.=
(b "\/" a) "/\" c
by Lem36X
.=
(a "\/" b) "/\" c
by A1
;
hence
(a "\/" b) "/\" c = (a "/\" c) "\/" (b "/\" c)
; verum