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
c8 is non empty ext-real-membered set
a is ext-real set
inf c8 is ext-real set
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