set F = the net_set of X,T;
take the net_set of X,T ; :: thesis: the net_set of X,T is yielding_non-empty_carriers
thus the net_set of X,T is yielding_non-empty_carriers ; :: thesis: verum