let x, y be Element of L; :: thesis: (((x `) "\/" (y `)) `) "\/" (((x `) "\/" y) `) = x
thus (((x `) "\/" (y `)) `) "\/" (((x `) "\/" y) `) = (x "/\" y) + (((x `) + y) `) by A1, Th33
.= (x + (((x `) + y) `)) "/\" (y + (((x `) + y) `)) by A1, LATTICES:11
.= (x + (((x `) + ((y `) `)) `)) "/\" (y + (((x `) + y) `)) by A1, Th32
.= (x + (x "/\" (y `))) "/\" (y + (((x `) + y) `)) by A1, Th33
.= x "/\" (y + (((x `) + y) `)) by LATTICES:def 8
.= x "/\" (y + (((x `) + ((y `) `)) `)) by A1, Th32
.= x "/\" (y + (x "/\" (y `))) by A1, Th33
.= x "/\" ((y + x) "/\" (y + (y `))) by A1, LATTICES:11
.= (x "/\" (y + x)) "/\" (y + (y `)) by LATTICES:def 7
.= x "/\" (y + (y `)) by LATTICES:def 9
.= x "/\" (Top L) by Th59
.= x by A2 ; :: thesis: verum