let L be GAD_Lattice; :: thesis: ( ( 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 ; :: thesis: for a, b, c being Element of L holds (a "\/" b) "/\" c = (b "\/" a) "/\" c
let a, b, c be Element of L; :: thesis: (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 )
proof
take d = c; :: thesis: ( (a "\/" b) "/\" c [= d & (b "\/" a) "/\" c [= d )
thus ( (a "\/" b) "/\" c [= d & (b "\/" a) "/\" c [= d ) by LATTICES:def 8; :: thesis: verum
end;
((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; :: thesis: verum