thus not len W is even by Def3; :: thesis: not len W is empty
hence not len W is empty by HEYTING3:1; :: thesis: verum