let R be non empty locally_directed Poset; :: thesis: for x, y being Element of R st ex z being Element of R st
( z <= x & z <= y ) holds
ex u being Element of R st
( x <= u & y <= u )
let x, y be Element of R; :: thesis: ( ex z being Element of R st
( z <= x & z <= y ) implies ex u being Element of R st
( x <= u & y <= u ) )
assume A1: ex z being Element of R st
( z <= x & z <= y ) ; :: thesis: ex u being Element of R st
( x <= u & y <= u )
reconsider x1 = x, y1 = y as Element of R ;
consider z being Element of R such that
A2: ( z <= x & z <= y ) by A1;
( CComp z = CComp x & CComp z = CComp y ) by A2, Th5;
then ( x in CComp z & y in CComp z ) by EQREL_1:28;
then ex u being Element of R st
( u in CComp z & x1 <= u & y1 <= u ) by WAYBEL_0:def 1;
hence ex u being Element of R st
( x <= u & y <= u ) ; :: thesis: verum