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