Net-Str D = Net-Str D,((id the carrier of S) | D) by Th9;
hence ( not Net-Str D is empty & Net-Str D is directed & Net-Str D is reflexive ) ; :: thesis: verum