let L be non empty LattStr ; :: thesis: ( L is trivial implies ( L is join-idempotent & L is meet-idempotent ) )
assume A1: L is trivial ; :: thesis: ( L is join-idempotent & L is meet-idempotent )
then for x being Element of L holds x "\/" x = x by STRUCT_0:def 10;
hence L is join-idempotent by ROBBINS1:def 7; :: thesis: L is meet-idempotent
for x being Element of L holds x "/\" x = x by A1, STRUCT_0:def 10;
hence L is meet-idempotent by SHEFFER1:def 9; :: thesis: verum