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