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