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