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

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