take ComplStr(# the carrier of TrivOrtLat ,the Compl of TrivOrtLat #) ; :: thesis: ( ComplStr(# the carrier of TrivOrtLat ,the Compl of TrivOrtLat #) is strict & not ComplStr(# the carrier of TrivOrtLat ,the Compl of TrivOrtLat #) is empty & ComplStr(# the carrier of TrivOrtLat ,the Compl of TrivOrtLat #) is trivial )
thus ( ComplStr(# the carrier of TrivOrtLat ,the Compl of TrivOrtLat #) is strict & not ComplStr(# the carrier of TrivOrtLat ,the Compl of TrivOrtLat #) is empty & ComplStr(# the carrier of TrivOrtLat ,the Compl of TrivOrtLat #) is trivial ) ; :: thesis: verum