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 "/\" k [= (i "/\" k) "\/" (i "/\" j) by LATTICES:22;
then A1: k [= i => ((i "/\" j) "\/" (i "/\" k)) by Def8;
i "/\" j [= (i "/\" j) "\/" (i "/\" k) by LATTICES:22;
then j [= i => ((i "/\" j) "\/" (i "/\" k)) by Def8;
then j "\/" k [= i => ((i "/\" j) "\/" (i "/\" k)) by A1, Th6;
then A2: i "/\" (j "\/" k) [= i "/\" (i => ((i "/\" j) "\/" (i "/\" k))) by LATTICES:27;
( i "/\" j [= i "/\" (j "\/" k) & i "/\" k [= i "/\" (j "\/" k) ) by LATTICES:22, LATTICES:27;
then A3: (i "/\" j) "\/" (i "/\" k) [= i "/\" (j "\/" k) by Th6;
i "/\" (i => ((i "/\" j) "\/" (i "/\" k))) [= (i "/\" j) "\/" (i "/\" k) by Def8;
then i "/\" (j "\/" k) [= (i "/\" j) "\/" (i "/\" k) by A2, LATTICES:25;
hence i "/\" (j "\/" k) = (i "/\" j) "\/" (i "/\" k) by A3, LATTICES:26; :: thesis: verum