let L be non empty reflexive transitive RelStr ; :: thesis: for D being non empty directed Subset of L holds Net-Str D in NetUniv L
let D be non empty directed Subset of L; :: thesis: Net-Str D in NetUniv L
A1: D in the_universe_of the carrier of L by Th24;
the carrier of (Net-Str D) = D by WAYBEL21:32;
hence Net-Str D in NetUniv L by A1, YELLOW_6:def 14; :: thesis: verum