let x be object ; :: thesis: for L being non empty RelStr
for J being non empty set
for K being ManySortedSet of J
for F being DoubleIndexedSet of K,L holds
( ( x in rng () implies ex j being Element of J st x = Sup ) & ( ex j being Element of J st x = Sup implies x in rng () ) & ( x in rng () implies ex j being Element of J st x = Inf ) & ( ex j being Element of J st x = Inf implies x in rng () ) )

let L be non empty RelStr ; :: thesis: for J being non empty set
for K being ManySortedSet of J
for F being DoubleIndexedSet of K,L holds
( ( x in rng () implies ex j being Element of J st x = Sup ) & ( ex j being Element of J st x = Sup implies x in rng () ) & ( x in rng () implies ex j being Element of J st x = Inf ) & ( ex j being Element of J st x = Inf implies x in rng () ) )

let J be non empty set ; :: thesis: for K being ManySortedSet of J
for F being DoubleIndexedSet of K,L holds
( ( x in rng () implies ex j being Element of J st x = Sup ) & ( ex j being Element of J st x = Sup implies x in rng () ) & ( x in rng () implies ex j being Element of J st x = Inf ) & ( ex j being Element of J st x = Inf implies x in rng () ) )

let K be ManySortedSet of J; :: thesis: for F being DoubleIndexedSet of K,L holds
( ( x in rng () implies ex j being Element of J st x = Sup ) & ( ex j being Element of J st x = Sup implies x in rng () ) & ( x in rng () implies ex j being Element of J st x = Inf ) & ( ex j being Element of J st x = Inf implies x in rng () ) )

let F be DoubleIndexedSet of K,L; :: thesis: ( ( x in rng () implies ex j being Element of J st x = Sup ) & ( ex j being Element of J st x = Sup implies x in rng () ) & ( x in rng () implies ex j being Element of J st x = Inf ) & ( ex j being Element of J st x = Inf implies x in rng () ) )
A1: dom F = J by PARTFUN1:def 2;
thus ( x in rng () iff ex j being Element of J st x = Sup ) :: thesis: ( x in rng () iff ex j being Element of J st x = Inf )
proof
hereby :: thesis: ( ex j being Element of J st x = Sup implies x in rng () )
assume x in rng () ; :: thesis: ex j being Element of J st x = Sup
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: x = Sup
thus x = Sup by A3; :: thesis: verum
end;
thus ( ex j being Element of J st x = Sup implies x in rng () ) by ; :: thesis: verum
end;
hereby :: thesis: ( ex j being Element of J st x = Inf implies x in rng () )
assume x in rng () ; :: thesis: ex j being Element of J st x = Inf
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: x = Inf
thus x = Inf by A5; :: thesis: verum
end;
thus ( ex j being Element of J st x = Inf implies x in rng () ) by ; :: thesis: verum