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