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_{1} being Element of the carrier of L st

( b_{1} in rng (netmap (N,L)) & x <= b_{1} & y <= b_{1} ) )

assume that

A2: x in rng (netmap (N,L)) and

A3: y in rng (netmap (N,L)) ; :: thesis: ex b_{1} being Element of the carrier of L st

( b_{1} in rng (netmap (N,L)) & x <= b_{1} & y <= b_{1} )

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

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

( b

assume that

A2: x in rng (netmap (N,L)) and

A3: y in rng (netmap (N,L)) ; :: thesis: ex b

( 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