consider x being Element of L;
downarrow x in { Y where Y is Ideal of L : verum } ;
hence not Ids L is empty ; :: thesis: verum