let R be non empty RelStr ; for S being non empty set
for f being Function of S, the carrier of R st rng f is directed holds
Net-Str (S,f) is directed
let S be non empty set ; for f being Function of S, the carrier of R st rng f is directed holds
Net-Str (S,f) is directed
let f be Function of S, the carrier of R; ( rng f is directed implies Net-Str (S,f) is directed )
assume A1:
rng f is directed
; Net-Str (S,f) is directed
set N = Net-Str (S,f);
let x, y be Element of (Net-Str (S,f)); YELLOW_6:def 3 ex b1 being Element of the carrier of (Net-Str (S,f)) st
( x <= b1 & y <= b1 )
f = the mapping of (Net-Str (S,f))
by Def10;
then A2:
rng f = { ((Net-Str (S,f)) . i) where i is Element of (Net-Str (S,f)) : verum }
by Th19;
then A3:
(Net-Str (S,f)) . x in rng f
;
(Net-Str (S,f)) . y in rng f
by A2;
then consider p being Element of R such that
A4:
p in rng f
and
A5:
(Net-Str (S,f)) . x <= p
and
A6:
(Net-Str (S,f)) . y <= p
by A1, A3;
consider z being object such that
A7:
z in dom f
and
A8:
p = f . z
by A4, FUNCT_1:def 3;
reconsider z = z as Element of (Net-Str (S,f)) by A7, Def10;
take
z
; ( x <= z & y <= z )
p = (Net-Str (S,f)) . z
by A8, Def10;
hence
( x <= z & y <= z )
by A5, A6, Def10; verum