Net-Str D = Net-Str (D,((id the carrier of S) | D)) by Th9;
hence Net-Str D is monotone ; :: thesis: verum