not 0_No == x by Def8;
hence x " is positive by Def8, Th40; :: thesis: verum