let x be object ; :: thesis:
let L be non empty RelStr ; :: thesis:
let J be non empty set ; :: thesis:
let K be ManySortedSet of J; :: thesis:
let F be DoubleIndexedSet of K,L; :: thesis:
A1: dom F = J by PARTFUN1:def 2;
thus ( x in rng (Sups ) iff ex j being Element of J st x = Sup ) :: thesis:

assume x in rng (Sups ) ; :: thesis:
then consider j being object such that
A2: j in dom F and
A3: x = \\/ ((F . j),L) by Th13;
reconsider j = j as Element of J by A2;
take j = j; :: thesis:
thus x = Sup by A3; :: thesis:

end;

end;

assume x in rng (Infs ) ; :: thesis:
then consider j being object such that
A4: j in dom F and
A5: x = //\ ((F . j),L) by Th13;
reconsider j = j as Element of J by A4;
take j = j; :: thesis:
thus x = Inf by A5; :: thesis:

end;