take TrivOrtLat ; :: thesis: ( TrivOrtLat is DeMorgan & TrivOrtLat is involutive & TrivOrtLat is bounded & TrivOrtLat is distributive & TrivOrtLat is Lattice-like )
thus ( TrivOrtLat is DeMorgan & TrivOrtLat is involutive & TrivOrtLat is bounded & TrivOrtLat is distributive & TrivOrtLat is Lattice-like ) ; :: thesis: verum