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

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