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 ; :: thesis: ( L is strict & L is 1 -element )
thus ( L is strict & L is 1 -element ) by STRUCT_0:def 19; :: thesis: verum