hereby :: thesis: ( ( for x, y being Element of N ex z being Element of N st
( x <= z & y <= z ) ) implies N is directed )

assume N is directed ; :: thesis: for x, y being Element of N ex z being Element of N st
( x <= z & y <= z )
then A1: [#] N is directed by WAYBEL_0:def 6;
let x, y be Element of N; :: thesis: ex z being Element of N st
( x <= z & y <= z )
ex z being Element of N st
( z in [#] N & x <= z & y <= z ) by A1, WAYBEL_0:def 1;
hence ex z being Element of N st
( x <= z & y <= z ) ; :: thesis: verum

end;

assume A2: for x, y being Element of N ex z being Element of N st
( x <= z & y <= z ) ; :: thesis: N is directed
let x, y be Element of N; :: according to WAYBEL_0:def 1,WAYBEL_0:def 6 :: thesis: ( not x in [#] N or not y in [#] N or ex b₁ being Element of the carrier of N st
( b₁ in [#] N & x <= b₁ & y <= b₁ ) )
assume ( x in [#] N & y in [#] N ) ; :: thesis: ex b₁ being Element of the carrier of N st
( b₁ in [#] N & x <= b₁ & y <= b₁ )
consider z being Element of N such that
A3: ( x <= z & y <= z ) by A2;
take z ; :: thesis: ( z in [#] N & x <= z & y <= z )
thus z in [#] N ; :: thesis: ( x <= z & y <= z )
thus ( x <= z & y <= z ) by A3; :: thesis: verum