set L = the finite distributive LATTICE;
take the finite distributive LATTICE ; :: thesis: ( the finite distributive LATTICE is lower-bounded & the finite distributive LATTICE is distributive & the finite distributive LATTICE is finite )
thus ( the finite distributive LATTICE is lower-bounded & the finite distributive LATTICE is distributive & the finite distributive LATTICE is finite ) ; :: thesis: verum