set N = Net-Str e;
the carrier of (Net-Str e) = {e} by Def11;
hence not the carrier of (Net-Str e) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum