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