take TrivComplLat ; :: thesis: ( TrivComplLat is join-commutative & TrivComplLat is join-associative & TrivComplLat is satisfying_DN_1 )
thus ( TrivComplLat is join-commutative & TrivComplLat is join-associative & TrivComplLat is satisfying_DN_1 ) ; :: thesis: verum