take TrivComplLat ; :: thesis: ( TrivComplLat is strict & not TrivComplLat is empty & TrivComplLat is trivial )
thus ( TrivComplLat is strict & not TrivComplLat is empty & TrivComplLat is trivial ) ; :: thesis: verum