take L = the trivial Lattice; :: thesis: ( L is satisfying_W3 & L is satisfying_W3' & L is join-idempotent & L is meet-idempotent & L is join-commutative & L is meet-commutative )
thus ( L is satisfying_W3 & L is satisfying_W3' & L is join-idempotent & L is meet-idempotent & L is join-commutative & L is meet-commutative ) by STRUCT_0:def 10; :: thesis: verum