for b₁, b₂ being Real
for b₃ being real number holds
( ( 0 < b₃ & b₁ in ].(b₂ - b₃),(b₂ + b₃).[ ) iff ex b₄ being Real st
( b₁ = b₂ + b₄ & abs b₄ < b₃ ) )

proof end;

theorem Th10: :: FCONT_3:10

for b₁, b₂ being Real
for b₃ being real number holds
( ( 0 < b₃ & b₁ in ].(b₂ - b₃),(b₂ + b₃).[ ) iff b₁ - b₂ in ].(- b₃),b₃.[ )

proof end;

theorem Th11: :: FCONT_3:11

for b₁ being Real holds left_closed_halfline b₁ = {b₁} \/ (left_open_halfline b₁)

proof end;

theorem Th12: :: FCONT_3:12

for b₁ being Real holds right_closed_halfline b₁ = {b₁} \/ (right_open_halfline b₁)

proof end;

theorem Th13: :: FCONT_3:13

for b₁ being Real
for b₂ being Real_Sequence
for b₃ being real number st ( for b₄ being Nat holds b₂ . b₄ = b₃ - (b₁ / (b₄ + 1)) ) holds
( b₂ is convergent & lim b₂ = b₃ )

proof end;

theorem Th14: :: FCONT_3:14

for b₁ being Real
for b₂ being Real_Sequence
for b₃ being real number st ( for b₄ being Nat holds b₂ . b₄ = b₃ + (b₁ / (b₄ + 1)) ) holds
( b₂ is convergent & lim b₂ = b₃ )

proof end;

theorem Th15: :: FCONT_3:15

for b₁ being Real
for b₂ being real number
for b₃ being PartFunc of REAL , REAL st b₃ is_continuous_in b₁ & b₃ . b₁ <> b₂ & ex b₄ being Neighbourhood of b₁ st b₄ c= dom b₃ holds
ex b₄ being Neighbourhood of b₁ st
( b₄ c= dom b₃ & ( for b₅ being Real st b₅ in b₄ holds
b₃ . b₅ <> b₂ ) )

proof end;

theorem Th16: :: FCONT_3:16

for b₁ being set
for b₂ being PartFunc of REAL , REAL st ( b₂ is_increasing_on b₁ or b₂ is_decreasing_on b₁ ) holds
b₂ | b₁ is one-to-one

proof end;

theorem Th17: :: FCONT_3:17

for b₁ being set
for b₂ being one-to-one PartFunc of REAL , REAL st b₂ is_increasing_on b₁ holds
(b₂ | b₁) " is_increasing_on b₂ .: b₁

proof end;

theorem Th18: :: FCONT_3:18

for b₁ being set
for b₂ being one-to-one PartFunc of REAL , REAL st b₂ is_decreasing_on b₁ holds
(b₂ | b₁) " is_decreasing_on b₂ .: b₁

proof end;

theorem Th19: :: FCONT_3:19

for b₁ being set
for b₂ being PartFunc of REAL , REAL st b₁ c= dom b₂ & b₂ is_monotone_on b₁ & ex b₃ being Real st b₂ .: b₁ = left_open_halfline b₃ holds
b₂ is_continuous_on b₁

proof end;

theorem Th20: :: FCONT_3:20

for b₁ being set
for b₂ being PartFunc of REAL , REAL st b₁ c= dom b₂ & b₂ is_monotone_on b₁ & ex b₃ being Real st b₂ .: b₁ = right_open_halfline b₃ holds
b₂ is_continuous_on b₁

proof end;

theorem Th21: :: FCONT_3:21

for b₁ being set
for b₂ being PartFunc of REAL , REAL st b₁ c= dom b₂ & b₂ is_monotone_on b₁ & ex b₃ being Real st b₂ .: b₁ = left_closed_halfline b₃ holds
b₂ is_continuous_on b₁

proof end;

theorem Th22: :: FCONT_3:22

for b₁ being set
for b₂ being PartFunc of REAL , REAL st b₁ c= dom b₂ & b₂ is_monotone_on b₁ & ex b₃ being Real st b₂ .: b₁ = right_closed_halfline b₃ holds
b₂ is_continuous_on b₁

proof end;

theorem Th23: :: FCONT_3:23

for b₁ being set
for b₂ being PartFunc of REAL , REAL st b₁ c= dom b₂ & b₂ is_monotone_on b₁ & ex b₃, b₄ being Real st b₂ .: b₁ = ].b₃,b₄.[ holds
b₂ is_continuous_on b₁

proof end;

theorem Th24: :: FCONT_3:24

for b₁ being set
for b₂ being PartFunc of REAL , REAL st b₁ c= dom b₂ & b₂ is_monotone_on b₁ & b₂ .: b₁ = REAL holds
b₂ is_continuous_on b₁

proof end;

theorem Th25: :: FCONT_3:25

for b₁, b₂ being Real
for b₃ being one-to-one PartFunc of REAL , REAL st ( b₃ is_increasing_on ].b₁,b₂.[ or b₃ is_decreasing_on ].b₁,b₂.[ ) & ].b₁,b₂.[ c= dom b₃ holds
(b₃ | ].b₁,b₂.[) " is_continuous_on b₃ .: ].b₁,b₂.[

proof end;

theorem Th26: :: FCONT_3:26

for b₁ being Real
for b₂ being one-to-one PartFunc of REAL , REAL st ( b₂ is_increasing_on left_open_halfline b₁ or b₂ is_decreasing_on left_open_halfline b₁ ) & left_open_halfline b₁ c= dom b₂ holds
(b₂ | (left_open_halfline b₁)) " is_continuous_on b₂ .: (left_open_halfline b₁)

proof end;

theorem Th27: :: FCONT_3:27

for b₁ being Real
for b₂ being one-to-one PartFunc of REAL , REAL st ( b₂ is_increasing_on right_open_halfline b₁ or b₂ is_decreasing_on right_open_halfline b₁ ) & right_open_halfline b₁ c= dom b₂ holds
(b₂ | (right_open_halfline b₁)) " is_continuous_on b₂ .: (right_open_halfline b₁)

proof end;

theorem Th28: :: FCONT_3:28

for b₁ being Real
for b₂ being one-to-one PartFunc of REAL , REAL st ( b₂ is_increasing_on left_closed_halfline b₁ or b₂ is_decreasing_on left_closed_halfline b₁ ) & left_closed_halfline b₁ c= dom b₂ holds
(b₂ | (left_closed_halfline b₁)) " is_continuous_on b₂ .: (left_closed_halfline b₁)

proof end;

theorem Th29: :: FCONT_3:29

for b₁ being Real
for b₂ being one-to-one PartFunc of REAL , REAL st ( b₂ is_increasing_on right_closed_halfline b₁ or b₂ is_decreasing_on right_closed_halfline b₁ ) & right_closed_halfline b₁ c= dom b₂ holds
(b₂ | (right_closed_halfline b₁)) " is_continuous_on b₂ .: (right_closed_halfline b₁)

proof end;

theorem Th30: :: FCONT_3:30

for b₁ being one-to-one PartFunc of REAL , REAL st ( b₁ is_increasing_on [#] REAL or b₁ is_decreasing_on [#] REAL ) & b₁ is total holds
b₁ " is_continuous_on rng b₁

proof end;

theorem Th31: :: FCONT_3:31

for b₁, b₂ being Real
for b₃ being PartFunc of REAL , REAL st b₃ is_continuous_on ].b₁,b₂.[ & ( b₃ is_increasing_on ].b₁,b₂.[ or b₃ is_decreasing_on ].b₁,b₂.[ ) holds
rng (b₃ | ].b₁,b₂.[) is open

proof end;

theorem Th32: :: FCONT_3:32

for b₁ being Real
for b₂ being PartFunc of REAL , REAL st b₂ is_continuous_on left_open_halfline b₁ & ( b₂ is_increasing_on left_open_halfline b₁ or b₂ is_decreasing_on left_open_halfline b₁ ) holds
rng (b₂ | (left_open_halfline b₁)) is open

proof end;

theorem Th33: :: FCONT_3:33

for b₁ being Real
for b₂ being PartFunc of REAL , REAL st b₂ is_continuous_on right_open_halfline b₁ & ( b₂ is_increasing_on right_open_halfline b₁ or b₂ is_decreasing_on right_open_halfline b₁ ) holds
rng (b₂ | (right_open_halfline b₁)) is open

proof end;

theorem Th34: :: FCONT_3:34

for b₁ being PartFunc of REAL , REAL st b₁ is_continuous_on [#] REAL & ( b₁ is_increasing_on [#] REAL or b₁ is_decreasing_on [#] REAL ) holds
rng b₁ is open

proof end;