let R be non empty transitive RelStr ; :: thesis: for S being non empty set
for f being Function of S, the carrier of R st S c= the carrier of R & Net-Str (S,f) is directed holds
Net-Str (S,f) in NetUniv R
let S be non empty set ; :: thesis: for f being Function of S, the carrier of R st S c= the carrier of R & Net-Str (S,f) is directed holds
Net-Str (S,f) in NetUniv R
let f be Function of S, the carrier of R; :: thesis: ( S c= the carrier of R & Net-Str (S,f) is directed implies Net-Str (S,f) in NetUniv R )
assume that
A1: S c= the carrier of R and
A2: Net-Str (S,f) is directed ; :: thesis: Net-Str (S,f) in NetUniv R
reconsider N = Net-Str (S,f) as strict net of R by A2;
set UN = the_universe_of the carrier of R;
reconsider UN = the_universe_of the carrier of R as universal set ;
the_transitive-closure_of the carrier of R in UN by CLASSES1:2;
then the carrier of R in UN by CLASSES1:3, CLASSES1:52;
then A3: S in UN by A1, CLASSES1:def 1;
the carrier of N = S by Def10;
hence Net-Str (S,f) in NetUniv R by A3, YELLOW_6:def 11; :: thesis: verum