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 5 :: 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 rng f = { ((Net-Str S,f) . i) where i is Element of (Net-Str S,f) : verum } by Th19;
then ( (Net-Str S,f) . x in rng f & (Net-Str S,f) . y in rng f ) ;
then consider p being Element of R such that
A2: p in rng f and
A3: ( (Net-Str S,f) . x <= p & (Net-Str S,f) . y <= p ) by A1, WAYBEL_0:def 1;
consider z being set such that
A4: z in dom f and
A5: p = f . z by A2, FUNCT_1:def 5;
reconsider z = z as Element of (Net-Str S,f) by A4, Def10;
take z ; :: thesis: ( x <= z & y <= z )
p = (Net-Str S,f) . z by A5, Def10;
hence ( x <= z & y <= z ) by A3, Def10; :: thesis: verum