set X = {{} };
consider XJ, XM being BinOp of {{} };
reconsider L = LattStr(# {{} },XJ,XM #) as non empty LattStr ;
A1: the carrier of L is trivial by REALSET1:def 4;
then A2: L is trivial ;
then A3: for a, b being Element of L holds a "\/" b = b "\/" a by STRUCT_0:def 10;
A4: for a, b, c being Element of L holds a "\/" (b "\/" c) = (a "\/" b) "\/" c by A2, STRUCT_0:def 10;
A5: for a, b being Element of L holds (a "/\" b) "\/" b = b by A2, STRUCT_0:def 10;
A6: for a, b being Element of L holds a "/\" b = b "/\" a by A2, STRUCT_0:def 10;
A7: for a, b, c being Element of L holds a "/\" (b "/\" c) = (a "/\" b) "/\" c by A2, STRUCT_0:def 10;
for a, b being Element of L holds a "/\" (a "\/" b) = a by A2, 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 A3, A4, A5, A6, A7, 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 & not L is empty & L is trivial )
thus ( L is strict & not L is empty & L is trivial ) by A1; :: thesis: verum