reconsider f = id the carrier of R as Function of the carrier of R,the carrier of R ;
rng f = [#] R by RELAT_1:71;
then reconsider N = Net-Str the carrier of R,f as reflexive strict net of R by Th20;
take N ; :: thesis: ( N is monotone & N is reflexive & N is strict )
thus ( N is monotone & N is reflexive & N is strict ) ; :: thesis: verum