( Roots X^3-2 <> {} implies X^3-2 is with_roots ) ;
hence Roots X^3-2 = {} by LL, thirred; :: thesis: verum