reconsider x9 = x as Element of L ;

thus not downarrow x is empty ; :: thesis: downarrow x is directed

let z, y be Element of L; :: according to WAYBEL_0:def 1 :: thesis: ( z in downarrow x & y in downarrow x implies ex z being Element of L st

( z in downarrow x & z <= z & y <= z ) )

assume that

A1: z in downarrow x and

A2: y in downarrow x ; :: thesis: ex z being Element of L st

( z in downarrow x & z <= z & y <= z )

take x9 ; :: thesis: ( x9 in downarrow x & z <= x9 & y <= x9 )

x9 <= x9 ;

hence ( x9 in downarrow x & z <= x9 & y <= x9 ) by A1, A2, Th17; :: thesis: verum

thus not downarrow x is empty ; :: thesis: downarrow x is directed

let z, y be Element of L; :: according to WAYBEL_0:def 1 :: thesis: ( z in downarrow x & y in downarrow x implies ex z being Element of L st

( z in downarrow x & z <= z & y <= z ) )

assume that

A1: z in downarrow x and

A2: y in downarrow x ; :: thesis: ex z being Element of L st

( z in downarrow x & z <= z & y <= z )

take x9 ; :: thesis: ( x9 in downarrow x & z <= x9 & y <= x9 )

x9 <= x9 ;

hence ( x9 in downarrow x & z <= x9 & y <= x9 ) by A1, A2, Th17; :: thesis: verum