ex f being Function of N,R st
( inf_net N = N *' f & ( for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) ) ) by Def4;
hence inf_net N is transitive ; :: thesis: verum