take ComplStr(# the carrier of TrivOrtLat, the Compl of TrivOrtLat #) ; :: thesis: ( ComplStr(# the carrier of TrivOrtLat, the Compl of TrivOrtLat #) is strict & ComplStr(# the carrier of TrivOrtLat, the Compl of TrivOrtLat #) is 1 -element )
thus ( ComplStr(# the carrier of TrivOrtLat, the Compl of TrivOrtLat #) is strict & ComplStr(# the carrier of TrivOrtLat, the Compl of TrivOrtLat #) is 1 -element ) ; :: thesis: verum