set X = {{}};
set XJ = the BinOp of {{}};
reconsider L = LattStr(# {{}}, the BinOp of {{}}, the BinOp of {{}} #) as non empty LattStr ;
A1:
L is trivial
;
then A2:
( ( for a, b being Element of L holds (a "/\" b) "\/" b = b ) & ( for a, b being Element of L holds a "/\" b = b "/\" a ) )
by STRUCT_0:def 10;
A3:
( ( for a, b, c being Element of L holds a "/\" (b "/\" c) = (a "/\" b) "/\" c ) & ( for a, b being Element of L holds a "/\" (a "\/" b) = a ) )
by A1, STRUCT_0:def 10;
( ( for a, b being Element of L holds a "\/" b = b "\/" a ) & ( for a, b, c being Element of L holds a "\/" (b "\/" c) = (a "\/" b) "\/" c ) )
by A1, STRUCT_0:def 10;
then
( L is join-commutative & L is join-associative & L is meet-absorbing & L is meet-commutative & L is meet-associative & L is join-absorbing )
by A2, A3, LATTICES:def 4, LATTICES:def 5, LATTICES:def 6, LATTICES:def 7, LATTICES:def 8, LATTICES:def 9;
then reconsider L = L as Lattice ;
take
L
; ( L is strict & L is 1 -element )
thus
( L is strict & L is 1 -element )
by STRUCT_0:def 19; verum