take TrivOrtLat ; :: thesis: ( TrivOrtLat is satisfying_DN_1 & TrivOrtLat is de_Morgan )
thus ( TrivOrtLat is satisfying_DN_1 & TrivOrtLat is de_Morgan ) ; :: thesis: verum