let L be Lattice; :: thesis: ( ( for a, b, c being Element of L holds ((a "/\" b) "\/" (b "/\" c)) "\/" (c "/\" a) = ((a "\/" b) "/\" (b "\/" c)) "/\" (c "\/" a) ) implies L is distributive )
assume A1: for a, b, c being Element of L holds ((a "/\" b) "\/" (b "/\" c)) "\/" (c "/\" a) = ((a "\/" b) "/\" (b "\/" c)) "/\" (c "\/" a) ; :: thesis: L is distributive
A2: now :: thesis: for a, b, c being Element of L st c [= a holds
a "/\" (b "\/" c) = (a "/\" b) "\/" c
let a, b, c be Element of L; :: thesis: ( c [= a implies a "/\" (b "\/" c) = (a "/\" b) "\/" c )
assume A3: c [= a ; :: thesis: a "/\" (b "\/" c) = (a "/\" b) "\/" c
thus a "/\" (b "\/" c) = (b "\/" c) "/\" (a "/\" (a "\/" b)) by Def9
.= (a "\/" b) "/\" ((b "\/" c) "/\" a) by Def7
.= (a "\/" b) "/\" ((b "\/" c) "/\" (c "\/" a)) by A3
.= ((a "\/" b) "/\" (b "\/" c)) "/\" (c "\/" a) by Def7
.= ((a "/\" b) "\/" (b "/\" c)) "\/" (c "/\" a) by A1
.= (a "/\" b) "\/" ((b "/\" c) "\/" (c "/\" a)) by Def5
.= (a "/\" b) "\/" ((b "/\" c) "\/" c) by A3, Th2
.= (a "/\" b) "\/" c by Def8 ; :: thesis: verum
end;
let a, b, c be Element of L; :: according to LATTICES:def 11 :: thesis: a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c)
A4: ((a "/\" b) "\/" (c "/\" a)) "\/" a = (a "/\" b) "\/" ((c "/\" a) "\/" a) by Def5
.= (a "/\" b) "\/" a by Def8
.= a by Def8 ;
thus a "/\" (b "\/" c) = (a "/\" (c "\/" a)) "/\" (b "\/" c) by Def9
.= a "/\" ((c "\/" a) "/\" (b "\/" c)) by Def7
.= (a "/\" (a "\/" b)) "/\" ((c "\/" a) "/\" (b "\/" c)) by Def9
.= a "/\" ((a "\/" b) "/\" ((b "\/" c) "/\" (c "\/" a))) by Def7
.= a "/\" (((a "\/" b) "/\" (b "\/" c)) "/\" (c "\/" a)) by Def7
.= a "/\" (((b "/\" c) "\/" (a "/\" b)) "\/" (c "/\" a)) by A1
.= a "/\" ((b "/\" c) "\/" ((a "/\" b) "\/" (c "/\" a))) by Def5
.= (a "/\" (b "/\" c)) "\/" ((a "/\" b) "\/" (c "/\" a)) by A2, A4, Def3
.= ((a "/\" b) "/\" c) "\/" ((a "/\" b) "\/" (c "/\" a)) by Def7
.= (((a "/\" b) "/\" c) "\/" (a "/\" b)) "\/" (c "/\" a) by Def5
.= (a "/\" b) "\/" (a "/\" c) by Def8 ; :: thesis: verum