let N be non empty RelStr ; :: thesis: ( N is directed iff RelStr(# the carrier of N,the InternalRel of N #) is directed )
thus ( N is directed implies RelStr(# the carrier of N,the InternalRel of N #) is directed ) :: thesis: ( RelStr(# the carrier of N,the InternalRel of N #) is directed implies N is directed )

proof

assume A1: N is directed ; :: thesis: RelStr(# the carrier of N,the InternalRel of N #) is directed
let x, y be Element of RelStr(# the carrier of N,the InternalRel of N #); :: according to YELLOW_6:def 5 :: thesis: ex z being Element of RelStr(# the carrier of N,the InternalRel of N #) st
( x <= z & y <= z )
reconsider x' = x, y' = y as Element of N ;
consider z' being Element of N such that
A2: ( x' <= z' & y' <= z' ) by A1, Def5;
reconsider z = z' as Element of RelStr(# the carrier of N,the InternalRel of N #) ;
take z ; :: thesis: ( x <= z & y <= z )
( [x,z] in the InternalRel of N & [y,z] in the InternalRel of N ) by A2, ORDERS_2:def 9;
hence ( x <= z & y <= z ) by ORDERS_2:def 9; :: thesis: verum

end;

assume A3: RelStr(# the carrier of N,the InternalRel of N #) is directed ; :: thesis: N is directed
let x, y be Element of N; :: according to YELLOW_6:def 5 :: thesis: ex z being Element of N st
( x <= z & y <= z )
reconsider x' = x, y' = y as Element of RelStr(# the carrier of N,the InternalRel of N #) ;
consider z' being Element of RelStr(# the carrier of N,the InternalRel of N #) such that
A4: ( x' <= z' & y' <= z' ) by A3, Def5;
reconsider z = z' as Element of N ;
take z ; :: thesis: ( x <= z & y <= z )
( [x',z'] in the InternalRel of RelStr(# the carrier of N,the InternalRel of N #) & [y',z'] in the InternalRel of RelStr(# the carrier of N,the InternalRel of N #) ) by A4, ORDERS_2:def 9;
hence ( x <= z & y <= z ) by ORDERS_2:def 9; :: thesis: verum