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
( D in the_universe_of the carrier of L & the carrier of (Net-Str D) = D ) by Th23, WAYBEL21:32;
hence Net-Str D in NetUniv L by YELLOW_6:def 11; :: thesis: verum