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 }
consider f being Function of N,R such that
A1: inf_net N = N *' f and
A2: for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) by Def4;
A3: 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;
A4: the mapping of (inf_net N) = f by A1, Def3;
then A5: 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 object ; :: 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 object such that
A6: u in dom f and
A7: e = f . u by A4, FUNCT_1:def 3;
reconsider u = u as Element of N by A6;
f . u = "/\" ( { (N . k) where k is Element of N : k >= u } ,R) by A2;
hence e in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } by A7; :: thesis: verum

end;

let e be object ; :: 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
A8: e = "/\" ( { (N . i) where i is Element of N : i >= j } ,R) ;
e = the mapping of (inf_net N) . j by A2, A4, A8;
hence e in rng the mapping of (inf_net N) by A3, A4, A5, FUNCT_1:def 3; :: thesis: verum