take TrivComplLat ; :: thesis: ( TrivComplLat is strict & TrivComplLat is join-associative & TrivComplLat is join-commutative & TrivComplLat is Robbins & TrivComplLat is join-idempotent & TrivComplLat is Huntington )
thus ( TrivComplLat is strict & TrivComplLat is join-associative & TrivComplLat is join-commutative & TrivComplLat is Robbins & TrivComplLat is join-idempotent & TrivComplLat is Huntington ) ; :: thesis: verum