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