let R be non empty RelStr ; :: thesis: for N being net of R holds rng the mapping of (inf_net N) = { ("/\" { (N . i) where i is Element of N : i >= j } ,R) where j is Element of N : verum }
let N be net of R; :: thesis: rng the mapping of (inf_net N) = { ("/\" { (N . i) where i is Element of N : i >= j } ,R) where j is Element of N : verum }
set X = { ("/\" { (N . i) where i is Element of N : i >= j } ,R) where j is Element of N : verum } ;
consider f being Function of N,R such that
A1: ( 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;
A2: RelStr(# the carrier of (inf_net N),the InternalRel of (inf_net N) #) = RelStr(# the carrier of N,the InternalRel of N #) by A1, Def3;
A3: the mapping of (inf_net N) = f by A1, Def3;
then A4: the carrier of (inf_net N) = dom f by FUNCT_2:def 1;
thus rng the mapping of (inf_net N) c= { ("/\" { (N . i) where i is Element of N : i >= j } ,R) where j is Element of N : verum } :: according to XBOOLE_0:def 10 :: thesis: { ("/\" { (N . i) where i is Element of N : i >= j } ,R) where j is Element of N : verum } c= rng the mapping of (inf_net N)

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in rng the mapping of (inf_net N) or e in { ("/\" { (N . i) where i is Element of N : i >= j } ,R) where j is Element of N : verum } )
assume e in rng the mapping of (inf_net N) ; :: thesis: e in { ("/\" { (N . i) where i is Element of N : i >= j } ,R) where j is Element of N : verum }
then consider u being set such that
A5: u in dom f and
A6: e = f . u by A3, FUNCT_1:def 5;
reconsider u = u as Element of N by A5;
f . u = "/\" { (N . k) where k is Element of N : k >= u } ,R by A1;
hence e in { ("/\" { (N . i) where i is Element of N : i >= j } ,R) where j is Element of N : verum } by A6; :: thesis: verum

end;

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in { ("/\" { (N . i) where i is Element of N : i >= j } ,R) where j is Element of N : verum } or e in rng the mapping of (inf_net N) )
assume e in { ("/\" { (N . i) where i is Element of N : i >= j } ,R) where j is Element of N : verum } ; :: thesis: e in rng the mapping of (inf_net N)
then consider j being Element of N such that
A7: e = "/\" { (N . i) where i is Element of N : i >= j } ,R ;
e = the mapping of (inf_net N) . j by A1, A3, A7;
hence e in rng the mapping of (inf_net N) by A2, A3, A4, FUNCT_1:def 5; :: thesis: verum