ex u being Element of V st u <> 0. V by Def18;
hence not NonZero V is empty by ZFMISC_1:56; :: thesis: verum