Bottom L << x by Th4;
hence not waybelow x is empty by Th7; :: thesis: verum