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

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