take L = the non empty trivial LattStr ; :: thesis: L is trivial
thus L is trivial ; :: thesis: verum