take TrivComplLat ; :: thesis: ( TrivComplLat is strict & TrivComplLat is 1 -element )
thus ( TrivComplLat is strict & TrivComplLat is 1 -element ) ; :: thesis: verum