consider N being net of R;
consider p being Element of R;
take N --> p ; :: thesis: ( N --> p is strict & N --> p is Function-yielding )
thus ( N --> p is strict & N --> p is Function-yielding ) ; :: thesis: verum