take the trivial Lattice ; :: thesis: ( the trivial Lattice is join-commutative & the trivial Lattice is join-associative & the trivial Lattice is join-idempotent & the trivial Lattice is meet-commutative & the trivial Lattice is meet-associative & the trivial Lattice is meet-idempotent & the trivial Lattice is satisfying_QLT1 & the trivial Lattice is satisfying_QLT2 )
thus ( the trivial Lattice is join-commutative & the trivial Lattice is join-associative & the trivial Lattice is join-idempotent & the trivial Lattice is meet-commutative & the trivial Lattice is meet-associative & the trivial Lattice is meet-idempotent & the trivial Lattice is satisfying_QLT1 & the trivial Lattice is satisfying_QLT2 ) ; :: thesis: verum