take
TrivOrtLat
; :: thesis: ( TrivOrtLat is satisfying_MD_1 & TrivOrtLat is satisfying_MD_2 & TrivOrtLat is satisfying_DN_1 & TrivOrtLat is de_Morgan )

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

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