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