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