let L be non empty LattStr ; :: thesis: ( L is trivial implies L is Lattice-like )
assume L is trivial ; :: thesis: L is Lattice-like
then reconsider LL = L as non empty trivial LattStr ;
( LL is meet-absorbing & LL is join-absorbing & LL is meet-commutative & LL is join-commutative & LL is meet-associative & LL is join-associative ) by STRUCT_0:def 10;
hence L is Lattice-like ; :: thesis: verum