let L be non empty RelStr ; :: thesis: for N being prenet of L st N is eventually-directed holds
rng (netmap N,L) is directed
let N be prenet of L; :: thesis: ( N is eventually-directed implies rng (netmap N,L) is directed )
assume A1: N is eventually-directed ; :: thesis: rng (netmap N,L) is directed
set f = netmap N,L;
let x, y be Element of L; :: according to WAYBEL_0:def 1 :: thesis: ( not x in rng (netmap N,L) or not y in rng (netmap N,L) or ex b₁ being Element of the carrier of L st
( b₁ in rng (netmap N,L) & x <= b₁ & y <= b₁ ) )
assume that
A2: x in rng (netmap N,L) and
A3: y in rng (netmap N,L) ; :: thesis: ex b₁ being Element of the carrier of L st
( b₁ in rng (netmap N,L) & x <= b₁ & y <= b₁ )
consider a being set such that
A4: ( a in dom (netmap N,L) & (netmap N,L) . a = x ) by A2, FUNCT_1:def 5;
consider b being set such that
A5: ( b in dom (netmap N,L) & (netmap N,L) . b = y ) by A3, FUNCT_1:def 5;
A6: dom (netmap N,L) = the carrier of N by FUNCT_2:def 1;
reconsider a = a, b = b as Element of N by A4, A5;
consider ja being Element of N such that
A7: for k being Element of N st ja <= k holds
N . a <= N . k by A1, WAYBEL_0:11;
consider jb being Element of N such that
A8: for k being Element of N st jb <= k holds
N . b <= N . k by A1, WAYBEL_0:11;
[#] N is directed by WAYBEL_0:def 6;
then consider c being Element of N such that
A10: ( c in [#] N & ja <= c & jb <= c ) by WAYBEL_0:def 1;
take z = (netmap N,L) . c; :: thesis: ( z in rng (netmap N,L) & x <= z & y <= z )
thus z in rng (netmap N,L) by A6, FUNCT_1:def 5; :: thesis: ( x <= z & y <= z )
( N . a = (netmap N,L) . a & N . b = (netmap N,L) . b & N . c = (netmap N,L) . c ) ;
hence ( x <= z & y <= z ) by A4, A5, A7, A8, A10; :: thesis: verum