let N be non empty directed RelStr ; :: 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 WAYBEL_0:def 6;

then ex z being Element of N st

( z in [#] N & x <= z & y <= z ) by WAYBEL_0:def 1;

hence ex z being Element of N st

( x <= z & y <= z ) ; :: thesis: verum

( 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 WAYBEL_0:def 6;

then ex z being Element of N st

( z in [#] N & x <= z & y <= z ) by WAYBEL_0:def 1;

hence ex z being Element of N st

( x <= z & y <= z ) ; :: thesis: verum