reconsider f = id the carrier of R as Function of the carrier of R, the carrier of R ;
rng f = [#] R by RELAT_1:45;
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