take <*0*> ; :: thesis: ( not <*0*> is empty & <*0*> is constant )
thus ( not <*0*> is empty & <*0*> is constant ) ; :: thesis: verum