take TrivOrtLat ; :: thesis: ( TrivOrtLat is strict & TrivOrtLat is Lattice-like & TrivOrtLat is Robbins & TrivOrtLat is Huntington )
thus ( TrivOrtLat is strict & TrivOrtLat is Lattice-like & TrivOrtLat is Robbins & TrivOrtLat is Huntington ) ; :: thesis: verum