begin
:: deftheorem Def14 defines SetMajorant SUPINF_1:def 1 :
for X, b2 being ext-real-membered set holds
( b2 = SetMajorant X iff for x being ext-real number holds
( x in b2 iff x is UpperBound of X ) );
theorem
:: deftheorem Def15 defines SetMinorant SUPINF_1:def 2 :
for X, b2 being ext-real-membered set holds
( b2 = SetMinorant X iff for x being ext-real number holds
( x in b2 iff x is LowerBound of X ) );
theorem
theorem
:: deftheorem Def19 defines SUP SUPINF_1:def 3 :
for F being bool_DOMAIN of ExtREAL
for b2 being ext-real-membered set holds
( b2 = SUP F iff for a being ext-real number holds
( a in b2 iff ex A being non empty ext-real-membered set st
( A in F & a = sup A ) ) );
theorem Th112:
theorem Th113:
theorem
:: deftheorem Def20 defines INF SUPINF_1:def 4 :
for F being bool_DOMAIN of ExtREAL
for b2 being ext-real-membered set holds
( b2 = INF F iff for a being ext-real number holds
( a in b2 iff ex A being non empty ext-real-membered set st
( A in F & a = inf A ) ) );
theorem Th117:
theorem Th118:
theorem