take TrivOrtLat ; :: thesis: ( TrivOrtLat is strict & TrivOrtLat is Boolean & TrivOrtLat is well-complemented )
thus ( TrivOrtLat is strict & TrivOrtLat is Boolean & TrivOrtLat is well-complemented ) ; :: thesis: verum