take TrivOrtLat ; :: thesis: ( TrivOrtLat is strict & TrivOrtLat is de_Morgan & TrivOrtLat is Boolean & TrivOrtLat is Robbins & TrivOrtLat is Huntington )
thus ( TrivOrtLat is strict & TrivOrtLat is de_Morgan & TrivOrtLat is Boolean & TrivOrtLat is Robbins & TrivOrtLat is Huntington ) ; :: thesis: verum