reconsider x' = x as Element of ;
thus not downarrow x is empty ; :: thesis: downarrow x is directed
let z, y be Element of ; :: according to WAYBEL_0:def 1 :: thesis: ( z in downarrow x & y in downarrow x implies ex z being Element of 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 st
( z in downarrow x & z <= z & y <= z )
take x' ; :: thesis: ( x' in downarrow x & z <= x' & y <= x' )
x' <= x' ;
hence ( x' in downarrow x & z <= x' & y <= x' ) by A1, A2, Th17; :: thesis: verum