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 object such that
A4: a in dom (netmap (N,L)) and
A5: (netmap (N,L)) . a = x by A2, FUNCT_1:def 3;
consider b being object such that
A6: b in dom (netmap (N,L)) and
A7: (netmap (N,L)) . b = y by A3, FUNCT_1:def 3;
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 ) ;
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 3; :: thesis: ( x <= z & y <= z )
N . c = (netmap (N,L)) . c ;
hence ( x <= z & y <= z ) by A5, A7, A8, A9, A10; :: thesis: verum