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:5;
then the carrier of R in UN by CLASSES1:6, CLASSES1:59;
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 14; :: thesis: verum