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 (Sups ) implies ex j being Element of J st x = Sup ) & ( ex j being Element of J st x = Sup implies x in rng (Sups ) ) & ( x in rng (Infs ) implies ex j being Element of J st x = Inf ) & ( ex j being Element of J st x = Inf implies x in rng (Infs ) ) )

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 (Sups ) implies ex j being Element of J st x = Sup ) & ( ex j being Element of J st x = Sup implies x in rng (Sups ) ) & ( x in rng (Infs ) implies ex j being Element of J st x = Inf ) & ( ex j being Element of J st x = Inf implies x in rng (Infs ) ) )

let J be non empty set ; :: thesis: for K being ManySortedSet of J

for F being DoubleIndexedSet of K,L holds

( ( x in rng (Sups ) implies ex j being Element of J st x = Sup ) & ( ex j being Element of J st x = Sup implies x in rng (Sups ) ) & ( x in rng (Infs ) implies ex j being Element of J st x = Inf ) & ( ex j being Element of J st x = Inf implies x in rng (Infs ) ) )

let K be ManySortedSet of J; :: thesis: for F being DoubleIndexedSet of K,L holds

( ( x in rng (Sups ) implies ex j being Element of J st x = Sup ) & ( ex j being Element of J st x = Sup implies x in rng (Sups ) ) & ( x in rng (Infs ) implies ex j being Element of J st x = Inf ) & ( ex j being Element of J st x = Inf implies x in rng (Infs ) ) )

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

A1: dom F = J by PARTFUN1:def 2;

thus ( x in rng (Sups ) iff ex j being Element of J st x = Sup ) :: thesis: ( x in rng (Infs ) iff ex j being Element of J st x = Inf )

for J being non empty set

for K being ManySortedSet of J

for F being DoubleIndexedSet of K,L holds

( ( x in rng (Sups ) implies ex j being Element of J st x = Sup ) & ( ex j being Element of J st x = Sup implies x in rng (Sups ) ) & ( x in rng (Infs ) implies ex j being Element of J st x = Inf ) & ( ex j being Element of J st x = Inf implies x in rng (Infs ) ) )

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 (Sups ) implies ex j being Element of J st x = Sup ) & ( ex j being Element of J st x = Sup implies x in rng (Sups ) ) & ( x in rng (Infs ) implies ex j being Element of J st x = Inf ) & ( ex j being Element of J st x = Inf implies x in rng (Infs ) ) )

let J be non empty set ; :: thesis: for K being ManySortedSet of J

for F being DoubleIndexedSet of K,L holds

( ( x in rng (Sups ) implies ex j being Element of J st x = Sup ) & ( ex j being Element of J st x = Sup implies x in rng (Sups ) ) & ( x in rng (Infs ) implies ex j being Element of J st x = Inf ) & ( ex j being Element of J st x = Inf implies x in rng (Infs ) ) )

let K be ManySortedSet of J; :: thesis: for F being DoubleIndexedSet of K,L holds

( ( x in rng (Sups ) implies ex j being Element of J st x = Sup ) & ( ex j being Element of J st x = Sup implies x in rng (Sups ) ) & ( x in rng (Infs ) implies ex j being Element of J st x = Inf ) & ( ex j being Element of J st x = Inf implies x in rng (Infs ) ) )

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

A1: dom F = J by PARTFUN1:def 2;

thus ( x in rng (Sups ) iff ex j being Element of J st x = Sup ) :: thesis: ( x in rng (Infs ) iff ex j being Element of J st x = Inf )

proof

end;

hereby :: thesis: ( ex j being Element of J st x = Sup implies x in rng (Sups ) )

thus
( ex j being Element of J st x = Sup implies x in rng (Sups ) )
by A1, Th13; :: thesis: verumassume
x in rng (Sups )
; :: 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;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

hereby :: thesis: ( ex j being Element of J st x = Inf implies x in rng (Infs ) )

thus
( ex j being Element of J st x = Inf implies x in rng (Infs ) )
by A1, Th13; :: thesis: verumassume
x in rng (Infs )
; :: 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;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