assume not downarrow X is empty ; :: thesis: contradiction
then consider x being object such that
A1: x in downarrow X by XBOOLE_0:def 1;
reconsider x = x as Element of L by A1;
ex z being Element of L st
( x <= z & z in X ) by A1, WAYBEL_0:def 15;
hence contradiction ; :: thesis: verum