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 A1: N is directed ; :: thesis: for x, y being Element of N ex z being Element of N st
( x <= z & y <= z )
let x, y be Element of N; :: thesis: ex z being Element of N st
( x <= z & y <= z )
[#] N is directed by A1;
then ex z being Element of N st
( z in [#] N & x <= z & y <= z ) ;
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 b1 being Element of the carrier of N st
( b1 in [#] N & x <= b1 & y <= b1 ) )
assume that
x in [#] N and
y in [#] N ; :: thesis: ex b1 being Element of the carrier of N st
( b1 in [#] N & x <= b1 & y <= b1 )
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