let R be non empty discrete Poset; :: thesis: R is locally_directed
let C be Component of R; :: according to OSALG_4:def 8 :: thesis: C is directed
consider x being Element of R such that
A1: C = {x} by Th7;
for x, y being Element of R st x in C & y in C holds
ex z being Element of R st
( z in C & x <= z & y <= z )
proof
let x1, y1 be Element of R; :: thesis: ( x1 in C & y1 in C implies ex z being Element of R st
( z in C & x1 <= z & y1 <= z ) )
assume that
A2: x1 in C and
A3: y1 in C ; :: thesis: ex z being Element of R st
( z in C & x1 <= z & y1 <= z )
take x1 ; :: thesis: ( x1 in C & x1 <= x1 & y1 <= x1 )
x1 = x by A1, A2, TARSKI:def 1;
hence ( x1 in C & x1 <= x1 & y1 <= x1 ) by A1, A3, TARSKI:def 1; :: thesis: verum
end;
hence C is directed by WAYBEL_0:def 1; :: thesis: verum