let L be non empty reflexive transitive RelStr ; :: thesis: for X being Subset of L holds
( X is directed iff downarrow X is directed )
let X be Subset of L; :: thesis: ( X is directed iff downarrow X is directed )
thus ( X is directed implies downarrow X is directed ) :: thesis: ( downarrow X is directed implies X is directed )

proof

assume A1: for x, y being Element of L st x in X & y in X holds
ex z being Element of L st
( z in X & x <= z & y <= z ) ; :: according to WAYBEL_0:def 1 :: thesis: downarrow X is directed
let x, y be Element of L; :: according to WAYBEL_0:def 1 :: thesis: ( x in downarrow X & y in downarrow X implies ex z being Element of L st
( z in downarrow X & x <= z & y <= z ) )
assume A2: ( x in downarrow X & y in downarrow X ) ; :: thesis: ex z being Element of L st
( z in downarrow X & x <= z & y <= z )
then consider x' being Element of L such that
A3: ( x <= x' & x' in X ) by Def15;
consider y' being Element of L such that
A4: ( y <= y' & y' in X ) by A2, Def15;
consider z being Element of L such that
A5: ( z in X & x' <= z & y' <= z ) by A1, A3, A4;
take z ; :: thesis: ( z in downarrow X & x <= z & y <= z )
z <= z ;
hence z in downarrow X by A5, Def15; :: thesis: ( x <= z & y <= z )
thus ( x <= z & y <= z ) by A3, A4, A5, ORDERS_2:26; :: thesis: verum

end;

set Y = downarrow X;
assume A6: for x, y being Element of L st x in downarrow X & y in downarrow X holds
ex z being Element of L st
( z in downarrow X & x <= z & y <= z ) ; :: according to WAYBEL_0:def 1 :: thesis: X is directed
let x, y be Element of L; :: according to WAYBEL_0:def 1 :: thesis: ( x in X & y in X implies ex z being Element of L st
( z in X & x <= z & y <= z ) )
assume A7: ( x in X & y in X ) ; :: thesis: ex z being Element of L st
( z in X & x <= z & y <= z )
( x <= x & y <= y ) ;
then ( x in downarrow X & y in downarrow X ) by A7, Def15;
then consider z being Element of L such that
A8: ( z in downarrow X & x <= z & y <= z ) by A6;
consider z' being Element of L such that
A9: ( z <= z' & z' in X ) by A8, Def15;
take z' ; :: thesis: ( z' in X & x <= z' & y <= z' )
thus z' in X by A9; :: thesis: ( x <= z' & y <= z' )
thus ( x <= z' & y <= z' ) by A8, A9, ORDERS_2:26; :: thesis: verum