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

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