take 0_. L ; :: thesis: 0_. L is with_roots
thus 0_. L is with_roots ; :: thesis: verum