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