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