take TrivOrtLat ; :: thesis: ( TrivOrtLat is involutive & TrivOrtLat is with_Top & TrivOrtLat is de_Morgan & TrivOrtLat is Lattice-like )
thus ( TrivOrtLat is involutive & TrivOrtLat is with_Top & TrivOrtLat is de_Morgan & TrivOrtLat is Lattice-like ) ; :: thesis: verum