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 ex z being Element of R st
( z <= x & z <= y ) ; :: thesis: ex u being Element of R st
( x <= u & y <= u )
then consider z being Element of R such that
A1: z <= x and
A2: z <= y ;
reconsider x1 = x, y1 = y as Element of R ;
CComp z = CComp y by A2, Th4;
then A3: y in CComp z by EQREL_1:20;
CComp z = CComp x by A1, Th4;
then x in CComp z by EQREL_1:20;
then ex u being Element of R st
( u in CComp z & x1 <= u & y1 <= u ) by A3, WAYBEL_0:def 1;
hence ex u being Element of R st
( x <= u & y <= u ) ; :: thesis: verum