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

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