let y, z be Element of L; :: according to WAYBEL_0:def 19 :: thesis: ( y in downarrow X & z <= y implies z in downarrow X )
assume y in downarrow X ; :: thesis: ( not z <= y or z in downarrow X )
then consider x being Element of L such that
A1: y <= x and
A2: x in X by Def15;
assume z <= y ; :: thesis: z in downarrow X
then z <= x by A1, ORDERS_2:3;
hence z in downarrow X by A2, Def15; :: thesis: verum