let y, z be Element of L; :: according to WAYBEL_0:def 20 :: thesis: ( y in uparrow X & y <= z implies z in uparrow X )
assume y in uparrow X ; :: thesis: ( not y <= z or z in uparrow X )
then consider x being Element of L such that
A2: ( y >= x & x in X ) by Def16;
assume z >= y ; :: thesis: z in uparrow X
then z >= x by A2, ORDERS_2:26;
hence z in uparrow X by A2, Def16; :: thesis: verum