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
A3: y >= x and
A4: x in X by Def16;
assume z >= y ; :: thesis: z in uparrow X
then z >= x by A3, ORDERS_2:3;
hence z in uparrow X by A4, Def16; :: thesis: verum