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) and
A5: (netmap N,L) . a = x by A2, FUNCT_1:def 5;
consider b being set such that
A6: b in dom (netmap N,L) and
A7: (netmap N,L) . b = y by A3, FUNCT_1:def 5;
reconsider a = a, b = b as Element of N by A4, A6;
consider ja being Element of N such that
A8: 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
A9: 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
c in [#] N and
A10: ( 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 )
dom (netmap N,L) = the carrier of N by FUNCT_2:def 1;
hence z in rng (netmap N,L) by FUNCT_1:def 5; :: thesis: ( x <= z & y <= z )
N . c = (netmap N,L) . c ;
hence ( x <= z & y <= z ) by A5, A7, A8, A9, A10; :: thesis: verum