set X = {{} };
consider XJ, XM being BinOp of {{} };
reconsider L = LattStr(# {{} },XJ,XM #) as non empty LattStr ;
A1: L is trivial by REALSET1:def 4;
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 & not L is empty & L is trivial )
thus ( L is strict & not L is empty & L is trivial ) by REALSET1:def 4; :: thesis: verum