consider L being finite distributive LATTICE;
take L ; :: thesis: ( L is lower-bounded & L is distributive & L is finite )
thus ( L is lower-bounded & L is distributive & L is finite ) ; :: thesis: verum