let R be non empty RelStr ; :: thesis: 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 ; :: thesis: 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; :: thesis: ( rng f is directed implies Net-Str (S,f) is directed )
assume A1: rng f is directed ; :: thesis: Net-Str (S,f) is directed
set N = Net-Str (S,f);
let x, y be Element of (Net-Str (S,f)); :: according to YELLOW_6:def 3 :: thesis: ex b₁ being Element of the carrier of (Net-Str (S,f)) st
( x <= b₁ & y <= b₁ )
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 ; :: thesis: ( x <= z & y <= z )
p = (Net-Str (S,f)) . z by A8, Def10;
hence ( x <= z & y <= z ) by A5, A6, Def10; :: thesis: verum