take id X ; :: thesis: ( not id X is empty & id X is V67() )
thus ( not id X is empty & id X is V67() ) ; :: thesis: verum