:: SUPINF_1 semantic presentation

REAL is non empty complex-membered ext-real-membered real-membered V21() set

K6(REAL) is non empty set

NAT is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() Element of K6(REAL)

ExtREAL is non empty ext-real-membered set

+infty is non empty ext-real positive non negative V14() set

-infty is non empty ext-real non positive negative V14() set

K33() is empty natural ext-real non positive non negative V14() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() Element of NAT

K23(K33(),REAL) is set

K21(K33(),REAL) is non empty set

K20(K33()) is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set

K21(K21(K33(),REAL),K20(K33())) is non empty set

K21(+infty,-infty) is non empty ext-real-membered set

REAL \/ K21(+infty,-infty) is non empty ext-real-membered set

{} is empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() set

F is ext-real-membered set

S is ext-real-membered set

a is ext-real set

b is ext-real set

S is ext-real-membered set

a is ext-real-membered set

b is ext-real set

F is ext-real-membered set

(F) is ext-real-membered set

the ext-real UpperBound of F is ext-real UpperBound of F

F is ext-real-membered set

S is ext-real-membered set

(S) is non empty ext-real-membered set

(F) is non empty ext-real-membered set

a is ext-real set

F is ext-real-membered set

S is ext-real-membered set

a is ext-real set

b is ext-real set

S is ext-real-membered set

a is ext-real-membered set

b is ext-real set

F is ext-real-membered set

(F) is ext-real-membered set

the ext-real LowerBound of F is ext-real LowerBound of F

F is ext-real-membered set

S is ext-real-membered set

(S) is non empty ext-real-membered set

(F) is non empty ext-real-membered set

a is ext-real set

F is non empty ext-real-membered set

sup F is ext-real set

(F) is non empty ext-real-membered set

inf (F) is ext-real set

inf F is ext-real set

(F) is non empty ext-real-membered set

sup (F) is ext-real set

S is ext-real set

S is ext-real set

F is non empty set

K6(F) is non empty set

K6(K6(F)) is non empty set

[#] F is non empty non proper Element of K6(F)

{([#] F)} is non empty Element of K6(K6(F))

K6(ExtREAL) is non empty set

K6(K6(ExtREAL)) is non empty set

F is non empty with_non-empty_elements Element of K6(K6(ExtREAL))

S is ext-real-membered set

a is ext-real-membered set

b is ext-real set

a is non empty ext-real-membered set

Z is ext-real set

sup a is ext-real set

S is ext-real-membered set

a is ext-real-membered set

b is ext-real set

Z is non empty ext-real-membered set

sup Z is ext-real set

Z is non empty ext-real-membered set

sup Z is ext-real set

F is non empty with_non-empty_elements Element of K6(K6(ExtREAL))

(F) is ext-real-membered set

the Element of F is Element of F

a is non empty ext-real-membered set

sup a is ext-real set

F is non empty with_non-empty_elements Element of K6(K6(ExtREAL))

union F is ext-real-membered Element of K6(ExtREAL)

(F) is non empty ext-real-membered set

S is non empty ext-real-membered set

sup S is ext-real set

a is ext-real set

b is non empty ext-real-membered set

sup b is ext-real set

Z is ext-real set

F is non empty with_non-empty_elements Element of K6(K6(ExtREAL))

union F is ext-real-membered Element of K6(ExtREAL)

(F) is non empty ext-real-membered set

sup (F) is ext-real set

S is ext-real-membered set

a is ext-real set

b is set

Z is non empty ext-real-membered set

sup Z is ext-real set

a is set

a is ext-real set

F is non empty with_non-empty_elements Element of K6(K6(ExtREAL))

union F is ext-real-membered Element of K6(ExtREAL)

(F) is non empty ext-real-membered set

sup (F) is ext-real set

S is non empty ext-real-membered set

sup S is ext-real set

F is non empty with_non-empty_elements Element of K6(K6(ExtREAL))

the Element of F is Element of F

b is ext-real-membered set

a is non empty ext-real-membered set

inf a is ext-real set

Z is non empty ext-real-membered set

a is ext-real set

c

a is ext-real set

inf c

S is ext-real-membered set

a is ext-real-membered set

b is set

Z is ext-real set

a is non empty ext-real-membered set

inf a is ext-real set

Z is ext-real set

a is non empty ext-real-membered set

inf a is ext-real set

F is non empty with_non-empty_elements Element of K6(K6(ExtREAL))

(F) is ext-real-membered set

the Element of F is Element of F

a is non empty ext-real-membered set

inf a is ext-real set

F is non empty with_non-empty_elements Element of K6(K6(ExtREAL))

union F is ext-real-membered Element of K6(ExtREAL)

(F) is non empty ext-real-membered set

S is non empty ext-real-membered set

inf S is ext-real set

a is ext-real set

b is non empty ext-real-membered set

inf b is ext-real set

Z is ext-real set

F is non empty with_non-empty_elements Element of K6(K6(ExtREAL))

union F is ext-real-membered Element of K6(ExtREAL)

(F) is non empty ext-real-membered set

inf (F) is ext-real set

S is ext-real-membered set

a is ext-real set

b is set

Z is non empty ext-real-membered set

inf Z is ext-real set

a is set

a is ext-real set

F is non empty with_non-empty_elements Element of K6(K6(ExtREAL))

union F is ext-real-membered Element of K6(ExtREAL)

(F) is non empty ext-real-membered set

inf (F) is ext-real set

S is non empty ext-real-membered set

inf S is ext-real set