let I be I_Lattice; :: thesis: I is distributive
let i be Element of I; :: according to LATTICES:def 11 :: thesis: for b₁, b₂ being Element of the carrier of I holds i "/\" (b₁ "\/" b₂) = (i "/\" b₁) "\/" (i "/\" b₂)
let j, k be Element of I; :: thesis: i "/\" (j "\/" k) = (i "/\" j) "\/" (i "/\" k)
( i "/\" j [= (i "/\" j) "\/" (i "/\" k) & i "/\" k [= (i "/\" k) "\/" (i "/\" j) & (i "/\" j) "\/" (i "/\" k) = (i "/\" k) "\/" (i "/\" j) ) by LATTICES:22;
then ( j [= i => ((i "/\" j) "\/" (i "/\" k)) & k [= i => ((i "/\" j) "\/" (i "/\" k)) ) by Def8;
then j "\/" k [= i => ((i "/\" j) "\/" (i "/\" k)) by Th6;
then ( i "/\" (j "\/" k) [= i "/\" (i => ((i "/\" j) "\/" (i "/\" k))) & i "/\" (i => ((i "/\" j) "\/" (i "/\" k))) [= (i "/\" j) "\/" (i "/\" k) ) by Def8, LATTICES:27;
then A1: i "/\" (j "\/" k) [= (i "/\" j) "\/" (i "/\" k) by LATTICES:25;
( i "/\" j [= i "/\" (j "\/" k) & i "/\" k [= i "/\" (j "\/" k) ) by LATTICES:22, LATTICES:27;
then (i "/\" j) "\/" (i "/\" k) [= i "/\" (j "\/" k) by Th6;
hence i "/\" (j "\/" k) = (i "/\" j) "\/" (i "/\" k) by A1, LATTICES:26; :: thesis: verum