consider F being net_set of X,T;
take F ; :: thesis: F is yielding_non-empty_carriers
thus F is yielding_non-empty_carriers ; :: thesis: verum