:: Basic Properties of Extended Real Numbers
:: by Andrzej Trybulec, Yatsuka Nakamura, Artur Korni{\l}owicz and
::
:: Received January 22, 2007
:: Copyright (c) 2007-2021 Association of Mizar Users


scheme :: XXREAL_1:sch 1
Conti{ P1[ object ], P2[ object ] } :
ex s being ExtReal st
( ( for r being ExtReal st P1[r] holds
r <= s ) & ( for r being ExtReal st P2[r] holds
s <= r ) )
provided
A1: for r, s being ExtReal st P1[r] & P2[s] holds
r <= s
proof end;

definition
let r, s be ExtReal;
func [.r,s.] -> set equals :: XXREAL_1:def 1
 { a where a is Element of ExtREAL : ( r <= a & a <= s ) } ;
correctness
coherence
{ a where a is Element of ExtREAL : ( r <= a & a <= s ) } is set ;
;
func [.r,s.[ -> set equals :: XXREAL_1:def 2
 { a where a is Element of ExtREAL : ( r <= a & a < s ) } ;
correctness
coherence
{ a where a is Element of ExtREAL : ( r <= a & a < s ) } is set ;
;
func ].r,s.] -> set equals :: XXREAL_1:def 3
 { a where a is Element of ExtREAL : ( r < a & a <= s ) } ;
correctness
coherence
{ a where a is Element of ExtREAL : ( r < a & a <= s ) } is set ;
;
func ].r,s.[ -> set equals :: XXREAL_1:def 4
 { a where a is Element of ExtREAL : ( r < a & a < s ) } ;
correctness
coherence
{ a where a is Element of ExtREAL : ( r < a & a < s ) } is set ;
;
end;

:: deftheorem defines [. XXREAL_1:def 1 :
for r, s being ExtReal holds [.r,s.] = { a where a is Element of ExtREAL : ( r <= a & a <= s ) } ;

:: deftheorem defines [. XXREAL_1:def 2 :
for r, s being ExtReal holds [.r,s.[ = { a where a is Element of ExtREAL : ( r <= a & a < s ) } ;

:: deftheorem defines ]. XXREAL_1:def 3 :
for r, s being ExtReal holds ].r,s.] = { a where a is Element of ExtREAL : ( r < a & a <= s ) } ;

:: deftheorem defines ]. XXREAL_1:def 4 :
for r, s being ExtReal holds ].r,s.[ = { a where a is Element of ExtREAL : ( r < a & a < s ) } ;

theorem Th1: :: XXREAL_1:1
for r, s, t being ExtReal holds
( t in [.r,s.] iff ( r <= t & t <= s ) )
proof end;

theorem Th2: :: XXREAL_1:2
for r, s, t being ExtReal holds
( t in ].r,s.] iff ( r < t & t <= s ) )
proof end;

theorem Th3: :: XXREAL_1:3
for r, s, t being ExtReal holds
( t in [.r,s.[ iff ( r <= t & t < s ) )
proof end;

theorem Th4: :: XXREAL_1:4
for r, s, t being ExtReal holds
( t in ].r,s.[ iff ( r < t & t < s ) )
proof end;

registration
let r, s be ExtReal;
cluster [.r,s.] -> ext-real-membered ;
coherence
[.r,s.] is ext-real-membered
proof end;
cluster [.r,s.[ -> ext-real-membered ;
coherence
[.r,s.[ is ext-real-membered
proof end;
cluster ].r,s.] -> ext-real-membered ;
coherence
].r,s.] is ext-real-membered
proof end;
cluster ].r,s.[ -> ext-real-membered ;
coherence
].r,s.[ is ext-real-membered
proof end;
end;

theorem Th5: :: XXREAL_1:5
for x being set
for p, q being ExtReal holds
( not x in [.p,q.] or x in ].p,q.[ or x = p or x = q )
proof end;

theorem Th6: :: XXREAL_1:6
for x being set
for p, q being ExtReal holds
( not x in [.p,q.] or x in ].p,q.] or x = p )
proof end;

theorem Th7: :: XXREAL_1:7
for x being set
for p, q being ExtReal holds
( not x in [.p,q.] or x in [.p,q.[ or x = q )
proof end;

theorem Th8: :: XXREAL_1:8
for x being set
for p, q being ExtReal holds
( not x in [.p,q.[ or x in ].p,q.[ or x = p )
proof end;

theorem Th9: :: XXREAL_1:9
for x being set
for p, q being ExtReal holds
( not x in ].p,q.] or x in ].p,q.[ or x = q )
proof end;

theorem :: XXREAL_1:10
for x being set
for p, q being ExtReal holds
( not x in [.p,q.[ or ( x in ].p,q.] & x <> q ) or x = p )
proof end;

theorem :: XXREAL_1:11
for x being set
for p, q being ExtReal holds
( not x in ].p,q.] or ( x in [.p,q.[ & x <> p ) or x = q )
proof end;

theorem Th12: :: XXREAL_1:12
for x being set
for p, q being ExtReal st x in ].p,q.] holds
( x in [.p,q.] & x <> p )
proof end;

theorem Th13: :: XXREAL_1:13
for x being set
for p, q being ExtReal st x in [.p,q.[ holds
( x in [.p,q.] & x <> q )
proof end;

theorem Th14: :: XXREAL_1:14
for x being set
for p, q being ExtReal st x in ].p,q.[ holds
( x in [.p,q.[ & x <> p )
proof end;

theorem Th15: :: XXREAL_1:15
for x being set
for p, q being ExtReal st x in ].p,q.[ holds
( x in ].p,q.] & x <> q )
proof end;

theorem Th16: :: XXREAL_1:16
for x being set
for p, q being ExtReal st x in ].p,q.[ holds
( x in [.p,q.] & x <> p & x <> q )
proof end;

theorem Th17: :: XXREAL_1:17
for r being ExtReal holds [.r,r.] = {r}
proof end;

theorem Th18: :: XXREAL_1:18
for r being ExtReal holds [.r,r.[ = {}
proof end;

theorem Th19: :: XXREAL_1:19
for r being ExtReal holds ].r,r.] = {}
proof end;

theorem Th20: :: XXREAL_1:20
for r being ExtReal holds ].r,r.[ = {}
proof end;

registration
let r be ExtReal;
cluster [.r,r.] -> non empty ;
coherence
not [.r,r.] is empty
proof end;
cluster [.r,r.[ -> empty ;
coherence
[.r,r.[ is empty by Th18;
cluster ].r,r.] -> empty ;
coherence
].r,r.] is empty by Th19;
cluster ].r,r.[ -> empty ;
coherence
].r,r.[ is empty by Th20;
end;

theorem Th21: :: XXREAL_1:21
for p, q being ExtReal holds ].p,q.[ c= ].p,q.]
proof end;

theorem Th22: :: XXREAL_1:22
for p, q being ExtReal holds ].p,q.[ c= [.p,q.[
proof end;

theorem Th23: :: XXREAL_1:23
for p, q being ExtReal holds ].p,q.] c= [.p,q.]
proof end;

theorem Th24: :: XXREAL_1:24
for p, q being ExtReal holds [.p,q.[ c= [.p,q.]
proof end;

theorem Th25: :: XXREAL_1:25
for p, q being ExtReal holds ].p,q.[ c= [.p,q.]
proof end;

theorem :: XXREAL_1:26
for p, q being ExtReal st p <= q holds
].q,p.] = {}
proof end;

theorem Th27: :: XXREAL_1:27
for p, q being ExtReal st p <= q holds
[.q,p.[ = {}
proof end;

theorem Th28: :: XXREAL_1:28
for p, q being ExtReal st p <= q holds
].q,p.[ = {}
proof end;

theorem Th29: :: XXREAL_1:29
for p, q being ExtReal st p < q holds
[.q,p.] = {}
proof end;

theorem :: XXREAL_1:30
for r, s being ExtReal st r <= s holds
not [.r,s.] is empty by Th1;

theorem :: XXREAL_1:31
for p, q being ExtReal st p < q holds
not [.p,q.[ is empty by Th3;

theorem :: XXREAL_1:32
for p, q being ExtReal st p < q holds
not ].p,q.] is empty by Th2;

theorem :: XXREAL_1:33
for p, q being ExtReal st p < q holds
not ].p,q.[ is empty
proof end;

theorem Th34: :: XXREAL_1:34
for p, q, r, s being ExtReal st p <= r & s <= q holds
[.r,s.] c= [.p,q.]
proof end;

theorem Th35: :: XXREAL_1:35
for p, q, r, s being ExtReal st p <= r & s <= q holds
[.r,s.[ c= [.p,q.]
proof end;

theorem Th36: :: XXREAL_1:36
for p, q, r, s being ExtReal st p <= r & s <= q holds
].r,s.] c= [.p,q.]
proof end;

theorem Th37: :: XXREAL_1:37
for p, q, r, s being ExtReal st p <= r & s <= q holds
].r,s.[ c= [.p,q.]
proof end;

theorem Th38: :: XXREAL_1:38
for p, q, r, s being ExtReal st p <= r & s <= q holds
[.r,s.[ c= [.p,q.[
proof end;

theorem Th39: :: XXREAL_1:39
for p, q, r, s being ExtReal st p < r & s <= q holds
[.r,s.] c= ].p,q.]
proof end;

theorem Th40: :: XXREAL_1:40
for p, q, r, s being ExtReal st p < r & s <= q holds
[.r,s.[ c= ].p,q.]
proof end;

theorem Th41: :: XXREAL_1:41
for p, q, r, s being ExtReal st p <= r & s <= q holds
].r,s.[ c= ].p,q.]
proof end;

theorem Th42: :: XXREAL_1:42
for p, q, r, s being ExtReal st p <= r & s <= q holds
].r,s.] c= ].p,q.]
proof end;

theorem Th43: :: XXREAL_1:43
for p, q, r, s being ExtReal st p <= r & s < q holds
[.r,s.] c= [.p,q.[
proof end;

theorem Th44: :: XXREAL_1:44
for p, q, r, s being ExtReal st p <= r & s < q holds
].r,s.] c= [.p,q.[
proof end;

theorem Th45: :: XXREAL_1:45
for p, q, r, s being ExtReal st p <= r & s <= q holds
].r,s.[ c= [.p,q.[
proof end;

theorem Th46: :: XXREAL_1:46
for p, q, r, s being ExtReal st p <= r & s <= q holds
].r,s.[ c= ].p,q.[
proof end;

theorem Th47: :: XXREAL_1:47
for p, q, r, s being ExtReal st p < r & s < q holds
[.r,s.] c= ].p,q.[
proof end;

theorem Th48: :: XXREAL_1:48
for p, q, r, s being ExtReal st p < r & s <= q holds
[.r,s.[ c= ].p,q.[
proof end;

theorem Th49: :: XXREAL_1:49
for p, q, r, s being ExtReal st p <= r & s < q holds
].r,s.] c= ].p,q.[
proof end;

theorem Th50: :: XXREAL_1:50
for p, q, r, s being ExtReal st r <= s & [.r,s.] c= [.p,q.] holds
( p <= r & s <= q )
proof end;

theorem Th51: :: XXREAL_1:51
for p, q, r, s being ExtReal st r < s & ].r,s.[ c= [.p,q.] holds
( p <= r & s <= q )
proof end;

theorem Th52: :: XXREAL_1:52
for p, q, r, s being ExtReal st r < s & [.r,s.[ c= [.p,q.] holds
( p <= r & s <= q )
proof end;

theorem Th53: :: XXREAL_1:53
for p, q, r, s being ExtReal st r < s & ].r,s.] c= [.p,q.] holds
( p <= r & s <= q )
proof end;

theorem Th54: :: XXREAL_1:54
for p, q, r, s being ExtReal st r <= s & [.r,s.] c= [.p,q.[ holds
( p <= r & s < q )
proof end;

theorem Th55: :: XXREAL_1:55
for p, q, r, s being ExtReal st r < s & [.r,s.[ c= [.p,q.[ holds
( p <= r & s <= q )
proof end;

theorem Th56: :: XXREAL_1:56
for p, q, r, s being ExtReal st r < s & ].r,s.[ c= [.p,q.[ holds
( p <= r & s <= q )
proof end;

theorem Th57: :: XXREAL_1:57
for p, q, r, s being ExtReal st r < s & ].r,s.] c= [.p,q.[ holds
( p <= r & s < q )
proof end;

theorem Th58: :: XXREAL_1:58
for p, q, r, s being ExtReal st r <= s & [.r,s.] c= ].p,q.] holds
( p < r & s <= q )
proof end;

theorem Th59: :: XXREAL_1:59
for p, q, r, s being ExtReal st r < s & ].r,s.[ c= ].p,q.] holds
( p <= r & s <= q )
proof end;

theorem Th60: :: XXREAL_1:60
for p, q, r, s being ExtReal st r < s & [.r,s.[ c= ].p,q.] holds
( p < r & s <= q )
proof end;

theorem Th61: :: XXREAL_1:61
for p, q, r, s being ExtReal st r < s & ].r,s.] c= ].p,q.] holds
( p <= r & s <= q )
proof end;

theorem Th62: :: XXREAL_1:62
for p, q, r, s being ExtReal st r <= s & [.r,s.] c= ].p,q.[ holds
( p < r & s < q )
proof end;

theorem Th63: :: XXREAL_1:63
for p, q, r, s being ExtReal st r < s & ].r,s.[ c= ].p,q.[ holds
( p <= r & s <= q )
proof end;

theorem Th64: :: XXREAL_1:64
for p, q, r, s being ExtReal st r < s & [.r,s.[ c= ].p,q.[ holds
( p < r & s <= q )
proof end;

theorem Th65: :: XXREAL_1:65
for p, q, r, s being ExtReal st r < s & ].r,s.] c= ].p,q.[ holds
( p <= r & s < q )
proof end;

theorem :: XXREAL_1:66
for p, q, r, s being ExtReal st p <= q & [.p,q.] = [.r,s.] holds
( p = r & q = s )
proof end;

theorem :: XXREAL_1:67
for p, q, r, s being ExtReal st p < q & ].p,q.[ = ].r,s.[ holds
( p = r & q = s )
proof end;

theorem :: XXREAL_1:68
for p, q, r, s being ExtReal st p < q & ].p,q.] = ].r,s.] holds
( p = r & q = s )
proof end;

theorem :: XXREAL_1:69
for p, q, r, s being ExtReal st p < q & [.p,q.[ = [.r,s.[ holds
( p = r & q = s )
proof end;

theorem :: XXREAL_1:70
for p, q, r, s being ExtReal st r <= s holds
[.r,s.] <> ].p,q.]
proof end;

theorem :: XXREAL_1:71
for p, q, r, s being ExtReal st r <= s holds
[.r,s.] <> [.p,q.[
proof end;

theorem :: XXREAL_1:72
for p, q, r, s being ExtReal st r <= s holds
[.r,s.] <> ].p,q.[
proof end;

theorem :: XXREAL_1:73
for p, q, r, s being ExtReal st r < s holds
[.r,s.[ <> [.p,q.]
proof end;

theorem :: XXREAL_1:74
for p, q, r, s being ExtReal st r < s holds
[.r,s.[ <> ].p,q.]
proof end;

theorem :: XXREAL_1:75
for p, q, r, s being ExtReal st r < s holds
[.r,s.[ <> ].p,q.[
proof end;

theorem :: XXREAL_1:76
for p, q, r, s being ExtReal st r < s holds
].r,s.] <> [.p,q.]
proof end;

theorem :: XXREAL_1:77
for p, q, r, s being ExtReal st r < s holds
].r,s.] <> [.p,q.[
proof end;

theorem :: XXREAL_1:78
for p, q, r, s being ExtReal st r < s holds
].r,s.] <> ].p,q.[
proof end;

theorem :: XXREAL_1:79
for p, q, r, s being ExtReal st r < s holds
].r,s.[ <> [.p,q.]
proof end;

theorem :: XXREAL_1:80
for p, q, r, s being ExtReal st r < s holds
].r,s.[ <> ].p,q.]
proof end;

theorem :: XXREAL_1:81
for p, q, r, s being ExtReal st r < s holds
].r,s.[ <> [.p,q.[
proof end;

theorem :: XXREAL_1:82
for p, q, r, s being ExtReal st r <= s & [.r,s.] c< [.p,q.] & not p < r holds
s < q
proof end;

theorem :: XXREAL_1:83
for p, q, r, s being ExtReal st r < s & ].r,s.[ c= [.p,q.] holds
[.r,s.] c= [.p,q.]
proof end;

theorem :: XXREAL_1:84
for p, r, s being ExtReal st r < s holds
[.s,p.[ c= ].r,p.[
proof end;

theorem Th85: :: XXREAL_1:85
for r, s being ExtReal st s <= r holds
( [.r,s.] c= {r} & [.r,s.] c= {s} )
proof end;

theorem :: XXREAL_1:86
for r, s being ExtReal holds ].r,s.[ misses {r,s}
proof end;

theorem :: XXREAL_1:87
for r, s being ExtReal holds [.r,s.[ misses {s}
proof end;

theorem :: XXREAL_1:88
for r, s being ExtReal holds ].r,s.] misses {r}
proof end;

theorem :: XXREAL_1:89
for p, q, r, s being ExtReal st s <= p holds
[.r,s.] misses ].p,q.[
proof end;

theorem :: XXREAL_1:90
for p, q, r, s being ExtReal st s <= p holds
[.r,s.] misses ].p,q.]
proof end;

theorem :: XXREAL_1:91
for p, q, r, s being ExtReal st s <= p holds
].r,s.] misses ].p,q.[
proof end;

theorem :: XXREAL_1:92
for p, q, r, s being ExtReal st s <= p holds
].r,s.] misses ].p,q.]
proof end;

theorem :: XXREAL_1:93
for p, q, r, s being ExtReal st s <= p holds
].r,s.[ misses [.p,q.]
proof end;

theorem :: XXREAL_1:94
for p, q, r, s being ExtReal st s <= p holds
].r,s.[ misses [.p,q.[
proof end;

theorem :: XXREAL_1:95
for p, q, r, s being ExtReal st s <= p holds
[.r,s.[ misses [.p,q.]
proof end;

theorem :: XXREAL_1:96
for p, q, r, s being ExtReal st s <= p holds
[.r,s.[ misses [.p,q.[
proof end;

theorem :: XXREAL_1:97
for p, q, r, s being ExtReal st r < p & r < s holds
not ].r,s.[ c= [.p,q.]
proof end;

theorem :: XXREAL_1:98
for p, q, r, s being ExtReal st r < p & r < s holds
not [.r,s.[ c= [.p,q.]
proof end;

theorem :: XXREAL_1:99
for p, q, r, s being ExtReal st r < p & r < s holds
not ].r,s.] c= [.p,q.]
proof end;

theorem :: XXREAL_1:100
for p, q, r, s being ExtReal st r < p & r <= s holds
not [.r,s.] c= [.p,q.]
proof end;

theorem :: XXREAL_1:101
for p, q, r, s being ExtReal st r < p & r < s holds
not ].r,s.[ c= [.p,q.[
proof end;

theorem :: XXREAL_1:102
for p, q, r, s being ExtReal st r < p & r < s holds
not ].r,s.] c= [.p,q.[
proof end;

theorem :: XXREAL_1:103
for p, q, r, s being ExtReal st r < p & r < s holds
not [.r,s.[ c= [.p,q.[
proof end;

theorem :: XXREAL_1:104
for p, q, r, s being ExtReal st r < p & r <= s holds
not [.r,s.] c= [.p,q.[
proof end;

theorem :: XXREAL_1:105
for p, q, r, s being ExtReal st r < p & r < s holds
not ].r,s.[ c= ].p,q.]
proof end;

theorem :: XXREAL_1:106
for p, q, r, s being ExtReal st r <= p & r < s holds
not [.r,s.[ c= ].p,q.]
proof end;

theorem :: XXREAL_1:107
for p, q, r, s being ExtReal st r < p & r < s holds
not ].r,s.] c= ].p,q.]
proof end;

theorem :: XXREAL_1:108
for p, q, r, s being ExtReal st r <= p & r <= s holds
not [.r,s.] c= ].p,q.]
proof end;

theorem :: XXREAL_1:109
for p, q, r, s being ExtReal st r <= p & r <= s holds
not [.r,s.] c= ].p,q.[
proof end;

theorem :: XXREAL_1:110
for p, q, r, s being ExtReal st r <= p & r < s holds
not [.r,s.[ c= ].p,q.[
proof end;

theorem :: XXREAL_1:111
for p, q, r, s being ExtReal st r < p & r < s holds
not ].r,s.] c= ].p,q.[
proof end;

theorem :: XXREAL_1:112
for p, q, r, s being ExtReal st r < p & r < s holds
not ].r,s.[ c= ].p,q.[
proof end;

theorem :: XXREAL_1:113
for p, q, r, s being ExtReal st q < s & r < s holds
not ].r,s.[ c= [.p,q.]
proof end;

theorem :: XXREAL_1:114
for p, q, r, s being ExtReal st q < s & r < s holds
not [.r,s.[ c= [.p,q.]
proof end;

theorem :: XXREAL_1:115
for p, q, r, s being ExtReal st q < s & r < s holds
not ].r,s.] c= [.p,q.]
proof end;

theorem :: XXREAL_1:116
for p, q, r, s being ExtReal st q < s & r <= s holds
not [.r,s.] c= [.p,q.]
proof end;

theorem :: XXREAL_1:117
for p, q, r, s being ExtReal st q < s & r < s holds
not ].r,s.[ c= [.p,q.[
proof end;

theorem :: XXREAL_1:118
for p, q, r, s being ExtReal st q <= s & r < s holds
not ].r,s.] c= [.p,q.[
proof end;

theorem :: XXREAL_1:119
for p, q, r, s being ExtReal st q < s & r < s holds
not [.r,s.[ c= [.p,q.[
proof end;

theorem :: XXREAL_1:120
for p, q, r, s being ExtReal st q < s & r < s holds
not ].r,s.[ c= ].p,q.]
proof end;

theorem :: XXREAL_1:121
for p, q, r, s being ExtReal st q < s & r <= s holds
not [.r,s.] c= ].p,q.]
proof end;

theorem :: XXREAL_1:122
for p, q, r, s being ExtReal st q < s & r < s holds
not [.r,s.[ c= ].p,q.]
proof end;

theorem :: XXREAL_1:123
for p, q, r, s being ExtReal st q < s & r < s holds
not ].r,s.] c= ].p,q.]
proof end;

theorem :: XXREAL_1:124
for p, q, r, s being ExtReal st q <= s & r <= s holds
not [.r,s.] c= ].p,q.[
proof end;

theorem :: XXREAL_1:125
for p, q, r, s being ExtReal st q < s & r < s holds
not [.r,s.[ c= ].p,q.[
proof end;

theorem :: XXREAL_1:126
for p, q, r, s being ExtReal st q <= s & r < s holds
not ].r,s.] c= ].p,q.[
proof end;

theorem :: XXREAL_1:127
for p, q, r, s being ExtReal st q < s & r < s holds
not ].r,s.[ c= ].p,q.[
proof end;

theorem Th128: :: XXREAL_1:128
for r, s being ExtReal st r <= s holds
[.r,s.] = ].r,s.[ \/ {r,s}
proof end;

theorem Th129: :: XXREAL_1:129
for r, s being ExtReal st r <= s holds
[.r,s.] = [.r,s.[ \/ {s}
proof end;

theorem Th130: :: XXREAL_1:130
for r, s being ExtReal st r <= s holds
[.r,s.] = {r} \/ ].r,s.]
proof end;

theorem Th131: :: XXREAL_1:131
for r, s being ExtReal st r < s holds
[.r,s.[ = {r} \/ ].r,s.[
proof end;

theorem Th132: :: XXREAL_1:132
for r, s being ExtReal st r < s holds
].r,s.] = ].r,s.[ \/ {s}
proof end;

theorem :: XXREAL_1:133
for r, s being ExtReal st r <= s holds
[.r,s.] \ {r,s} = ].r,s.[
proof end;

theorem :: XXREAL_1:134
for r, s being ExtReal st r <= s holds
[.r,s.] \ {r} = ].r,s.]
proof end;

theorem :: XXREAL_1:135
for r, s being ExtReal st r <= s holds
[.r,s.] \ {s} = [.r,s.[
proof end;

theorem :: XXREAL_1:136
for r, s being ExtReal st r < s holds
[.r,s.[ \ {r} = ].r,s.[
proof end;

theorem :: XXREAL_1:137
for r, s being ExtReal st r < s holds
].r,s.] \ {s} = ].r,s.[
proof end;

theorem :: XXREAL_1:138
for r, s, t being ExtReal st r < s & s < t holds
].r,s.] /\ [.s,t.[ = {s}
proof end;

theorem :: XXREAL_1:139
for p, q, r, s being ExtReal holds [.r,s.[ /\ [.p,q.[ = [.(max (r,p)),(min (s,q)).[
proof end;

theorem :: XXREAL_1:140
for p, q, r, s being ExtReal holds [.r,s.] /\ [.p,q.] = [.(max (r,p)),(min (s,q)).]
proof end;

theorem :: XXREAL_1:141
for p, q, r, s being ExtReal holds ].r,s.] /\ ].p,q.] = ].(max (r,p)),(min (s,q)).]
proof end;

theorem :: XXREAL_1:142
for p, q, r, s being ExtReal holds ].r,s.[ /\ ].p,q.[ = ].(max (r,p)),(min (s,q)).[
proof end;

theorem :: XXREAL_1:143
for p, q, r, s being ExtReal st r <= p & s <= q holds
[.r,s.] /\ [.p,q.] = [.p,s.]
proof end;

theorem :: XXREAL_1:144
for p, q, r, s being ExtReal st r <= p & s <= q holds
[.r,s.[ /\ [.p,q.] = [.p,s.[
proof end;

theorem :: XXREAL_1:145
for p, q, r, s being ExtReal st r >= p & s > q holds
[.r,s.[ /\ [.p,q.] = [.r,q.]
proof end;

theorem :: XXREAL_1:146
for p, q, r, s being ExtReal st r < p & s <= q holds
].r,s.] /\ [.p,q.] = [.p,s.]
proof end;

theorem :: XXREAL_1:147
for p, q, r, s being ExtReal st r >= p & s >= q holds
].r,s.] /\ [.p,q.] = ].r,q.]
proof end;

theorem :: XXREAL_1:148
for p, q, r, s being ExtReal st r < p & s <= q holds
].r,s.[ /\ [.p,q.] = [.p,s.[
proof end;

theorem :: XXREAL_1:149
for p, q, r, s being ExtReal st r >= p & s > q holds
].r,s.[ /\ [.p,q.] = ].r,q.]
proof end;

theorem :: XXREAL_1:150
for p, q, r, s being ExtReal st r <= p & s <= q holds
[.r,s.[ /\ [.p,q.[ = [.p,s.[
proof end;

theorem :: XXREAL_1:151
for p, q, r, s being ExtReal st r >= p & s >= q holds
[.r,s.[ /\ [.p,q.[ = [.r,q.[
proof end;

theorem Th152: :: XXREAL_1:152
for p, q, r, s being ExtReal st r < p & s < q holds
].r,s.] /\ [.p,q.[ = [.p,s.]
proof end;

theorem :: XXREAL_1:153
for p, q, r, s being ExtReal st r >= p & s >= q holds
].r,s.] /\ [.p,q.[ = ].r,q.[
proof end;

theorem Th154: :: XXREAL_1:154
for p, q, r, s being ExtReal st r < p & s <= q holds
].r,s.[ /\ [.p,q.[ = [.p,s.[
proof end;

theorem :: XXREAL_1:155
for p, q, r, s being ExtReal st r >= p & s >= q holds
].r,s.[ /\ [.p,q.[ = ].r,q.[
proof end;

theorem :: XXREAL_1:156
for p, q, r, s being ExtReal st r <= p & s <= q holds
].r,s.] /\ ].p,q.] = ].p,s.]
proof end;

theorem :: XXREAL_1:157
for p, q, r, s being ExtReal st r >= p & s >= q holds
].r,s.] /\ ].p,q.] = ].r,q.]
proof end;

theorem :: XXREAL_1:158
for p, q, r, s being ExtReal st r <= p & s <= q holds
].r,s.[ /\ ].p,q.] = ].p,s.[
proof end;

theorem Th159: :: XXREAL_1:159
for p, q, r, s being ExtReal st r >= p & s > q holds
].r,s.[ /\ ].p,q.] = ].r,q.]
proof end;

theorem Th160: :: XXREAL_1:160
for p, q, r, s being ExtReal st r <= p & s <= q holds
].r,s.[ /\ ].p,q.[ = ].p,s.[
proof end;

theorem :: XXREAL_1:161
for p, q, r, s being ExtReal holds [.r,s.[ \/ [.p,q.[ c= [.(min (r,p)),(max (s,q)).[
proof end;

theorem :: XXREAL_1:162
for p, q, r, s being ExtReal st [.r,s.[ meets [.p,q.[ holds
[.r,s.[ \/ [.p,q.[ = [.(min (r,p)),(max (s,q)).[
proof end;

theorem :: XXREAL_1:163
for p, q, r, s being ExtReal holds ].r,s.] \/ ].p,q.] c= ].(min (r,p)),(max (s,q)).]
proof end;

theorem :: XXREAL_1:164
for p, q, r, s being ExtReal st ].r,s.] meets ].p,q.] holds
].r,s.] \/ ].p,q.] = ].(min (r,p)),(max (s,q)).]
proof end;

theorem :: XXREAL_1:165
for r, s, t being ExtReal st r <= s & s <= t holds
[.r,s.] \/ [.s,t.] = [.r,t.]
proof end;

theorem Th166: :: XXREAL_1:166
for r, s, t being ExtReal st r <= s & s <= t holds
[.r,s.[ \/ [.s,t.] = [.r,t.]
proof end;

theorem Th167: :: XXREAL_1:167
for r, s, t being ExtReal st r <= s & s <= t holds
[.r,s.] \/ ].s,t.] = [.r,t.]
proof end;

theorem :: XXREAL_1:168
for r, s, t being ExtReal st r <= s & s <= t holds
[.r,s.[ \/ [.s,t.[ = [.r,t.[
proof end;

theorem Th169: :: XXREAL_1:169
for r, s, t being ExtReal st r <= s & s < t holds
[.r,s.] \/ ].s,t.[ = [.r,t.[
proof end;

theorem :: XXREAL_1:170
for r, s, t being ExtReal st r <= s & s <= t holds
].r,s.] \/ ].s,t.] = ].r,t.]
proof end;

theorem Th171: :: XXREAL_1:171
for r, s, t being ExtReal st r <= s & s < t holds
].r,s.] \/ ].s,t.[ = ].r,t.[
proof end;

theorem :: XXREAL_1:172
for r, s, t being ExtReal st r < s & s < t holds
].r,s.] \/ [.s,t.[ = ].r,t.[
proof end;

theorem Th173: :: XXREAL_1:173
for r, s, t being ExtReal st r < s & s < t holds
].r,s.[ \/ [.s,t.[ = ].r,t.[
proof end;

theorem Th174: :: XXREAL_1:174
for p, q, r, s being ExtReal st p <= s & r <= q & s <= r holds
[.p,r.] \/ [.s,q.] = [.p,q.]
proof end;

theorem Th175: :: XXREAL_1:175
for p, q, r, s being ExtReal st p <= s & r <= q & s < r holds
[.p,r.[ \/ ].s,q.] = [.p,q.]
proof end;

theorem :: XXREAL_1:176
for p, q, r, s being ExtReal st p <= s & s <= r & r < q holds
[.p,r.] \/ [.s,q.[ = [.p,q.[
proof end;

theorem :: XXREAL_1:177
for p, q, r, s being ExtReal st p < s & r <= q & s <= r holds
].p,r.] \/ [.s,q.] = ].p,q.]
proof end;

theorem Th178: :: XXREAL_1:178
for p, q, r, s being ExtReal st p < s & r < q & s <= r holds
].p,r.] \/ [.s,q.[ = ].p,q.[
proof end;

theorem :: XXREAL_1:179
for p, q, r, s being ExtReal st p <= r & p <= s & r <= q & s <= q holds
([.p,r.[ \/ [.r,s.]) \/ ].s,q.] = [.p,q.]
proof end;

theorem :: XXREAL_1:180
for p, q, r, s being ExtReal st p < r & p < s & r < q & s < q holds
(].p,r.] \/ ].r,s.[) \/ [.s,q.[ = ].p,q.[
proof end;

theorem :: XXREAL_1:181
for p, q, r, s being ExtReal st p <= r & r <= s & s <= q holds
([.p,r.] \/ ].r,s.[) \/ [.s,q.] = [.p,q.]
proof end;

theorem Th182: :: XXREAL_1:182
for r, s, t being ExtReal st r <= s holds
[.r,t.] \ [.r,s.] = ].s,t.]
proof end;

theorem Th183: :: XXREAL_1:183
for r, s, t being ExtReal st r <= s holds
[.r,t.[ \ [.r,s.] = ].s,t.[
proof end;

theorem Th184: :: XXREAL_1:184
for r, s, t being ExtReal st r < s holds
[.r,t.] \ [.r,s.[ = [.s,t.]
proof end;

theorem Th185: :: XXREAL_1:185
for r, s, t being ExtReal st r < s holds
[.r,t.[ \ [.r,s.[ = [.s,t.[
proof end;

theorem Th186: :: XXREAL_1:186
for r, s, t being ExtReal st r <= s holds
[.r,t.] \ [.r,s.] = ].s,t.]
proof end;

theorem Th187: :: XXREAL_1:187
for r, s, t being ExtReal st r < s holds
].r,t.[ \ ].r,s.] = ].s,t.[
proof end;

theorem Th188: :: XXREAL_1:188
for r, s, t being ExtReal st r < s holds
].r,t.] \ ].r,s.[ = [.s,t.]
proof end;

theorem Th189: :: XXREAL_1:189
for r, s, t being ExtReal st r < s holds
].r,t.[ \ ].r,s.[ = [.s,t.[
proof end;

theorem Th190: :: XXREAL_1:190
for r, s, t being ExtReal st s <= t holds
[.r,t.] \ [.s,t.] = [.r,s.[
proof end;

theorem Th191: :: XXREAL_1:191
for r, s, t being ExtReal st s <= t holds
].r,t.] \ [.s,t.] = ].r,s.[
proof end;

theorem Th192: :: XXREAL_1:192
for r, s, t being ExtReal st s < t holds
[.r,t.] \ ].s,t.] = [.r,s.]
proof end;

theorem Th193: :: XXREAL_1:193
for r, s, t being ExtReal st s < t holds
].r,t.] \ ].s,t.] = ].r,s.]
proof end;

theorem Th194: :: XXREAL_1:194
for r, s, t being ExtReal st s < t holds
[.r,t.[ \ [.s,t.[ = [.r,s.[
proof end;

theorem Th195: :: XXREAL_1:195
for r, s, t being ExtReal st s < t holds
].r,t.[ \ [.s,t.[ = ].r,s.[
proof end;

theorem Th196: :: XXREAL_1:196
for r, s, t being ExtReal st s < t holds
[.r,t.[ \ ].s,t.[ = [.r,s.]
proof end;

theorem Th197: :: XXREAL_1:197
for r, s, t being ExtReal st s < t holds
].r,t.[ \ ].s,t.[ = ].r,s.]
proof end;

theorem :: XXREAL_1:198
for p, q, r, s being ExtReal st [.p,q.[ meets [.r,s.[ holds
[.p,q.[ \ [.r,s.[ = [.p,r.[ \/ [.s,q.[
proof end;

theorem :: XXREAL_1:199
for p, q, r, s being ExtReal st ].p,q.] meets ].r,s.] holds
].p,q.] \ ].r,s.] = ].p,r.] \/ ].s,q.]
proof end;

theorem :: XXREAL_1:200
for p, q, r, s being ExtReal st p <= r & s <= q holds
[.p,q.] \ ([.p,r.] \/ [.s,q.]) = ].r,s.[
proof end;

theorem :: XXREAL_1:201
for r, s, t being ExtReal st r <= s & s <= t holds
[.r,t.] \ {s} = [.r,s.[ \/ ].s,t.]
proof end;

theorem :: XXREAL_1:202
for r, s, t being ExtReal st r <= s & s < t holds
[.r,t.[ \ {s} = [.r,s.[ \/ ].s,t.[
proof end;

theorem :: XXREAL_1:203
for r, s, t being ExtReal st r < s & s <= t holds
].r,t.] \ {s} = ].r,s.[ \/ ].s,t.]
proof end;

theorem :: XXREAL_1:204
for r, s, t being ExtReal st r < s & s < t holds
].r,t.[ \ {s} = ].r,s.[ \/ ].s,t.[
proof end;

theorem :: XXREAL_1:205
for r, s, t being ExtReal holds not s in ].r,s.[ \/ ].s,t.[
proof end;

theorem :: XXREAL_1:206
for r, s, t being ExtReal holds not s in [.r,s.[ \/ ].s,t.[
proof end;

theorem :: XXREAL_1:207
for r, s, t being ExtReal holds not s in ].r,s.[ \/ ].s,t.]
proof end;

theorem :: XXREAL_1:208
for r, s, t being ExtReal holds not s in [.r,s.[ \/ ].s,t.]
proof end;

theorem :: XXREAL_1:209
[.-infty,+infty.] = ExtREAL
proof end;

theorem :: XXREAL_1:210
for p being ExtReal holds ].p,-infty.[ = {}
proof end;

theorem :: XXREAL_1:211
for p being ExtReal holds [.p,-infty.[ = {}
proof end;

theorem :: XXREAL_1:212
for p being ExtReal holds ].p,-infty.] = {}
proof end;

theorem :: XXREAL_1:213
for p being ExtReal st p <> -infty holds
[.p,-infty.] = {}
proof end;

theorem :: XXREAL_1:214
for p being ExtReal holds ].+infty,p.[ = {}
proof end;

theorem :: XXREAL_1:215
for p being ExtReal holds [.+infty,p.[ = {}
proof end;

theorem :: XXREAL_1:216
for p being ExtReal holds ].+infty,p.] = {}
proof end;

theorem :: XXREAL_1:217
for p being ExtReal st p <> +infty holds
[.+infty,p.] = {}
proof end;

theorem :: XXREAL_1:218
for p, q being ExtReal st p > q holds
p in ].q,+infty.] by XXREAL_0:3, Th2;

theorem :: XXREAL_1:219
for p, q being ExtReal st q <= p holds
p in [.q,+infty.]
proof end;

theorem :: XXREAL_1:220
for p, q being ExtReal st p <= q holds
p in [.-infty,q.]
proof end;

theorem :: XXREAL_1:221
for p, q being ExtReal st p < q holds
p in [.-infty,q.[ by XXREAL_0:5, Th3;

theorem :: XXREAL_1:222
for p, q being ExtReal st p <= q holds
[.p,q.] = [.p,q.] \/ [.q,p.]
proof end;

theorem :: XXREAL_1:223
for p, r, s, t being ExtReal st r <= s & s <= t holds
not r in ].s,t.[ \/ ].t,p.[
proof end;

:: from LIMFUNC1, 2008.06.12, A.T.
theorem Th224: :: XXREAL_1:224
REAL = ].-infty,+infty.[
proof end;

theorem Th225: :: XXREAL_1:225
for p, q being ExtReal holds ].p,q.[ c= REAL
proof end;

theorem Th226: :: XXREAL_1:226
for p, q being ExtReal st p in REAL holds
[.p,q.[ c= REAL
proof end;

theorem Th227: :: XXREAL_1:227
for p, q being ExtReal st q in REAL holds
].p,q.] c= REAL
proof end;

theorem Th228: :: XXREAL_1:228
for p, q being ExtReal st p in REAL & q in REAL holds
[.p,q.] c= REAL
proof end;

registration
let p, q be ExtReal;
cluster ].p,q.[ -> real-membered ;
coherence
].p,q.[ is real-membered by Th225, MEMBERED:21;
end;

registration
let p be Real;
let q be ExtReal;
cluster [.p,q.[ -> real-membered ;
coherence
[.p,q.[ is real-membered
proof end;
end;

registration
let q be Real;
let p be ExtReal;
cluster ].p,q.] -> real-membered ;
coherence
].p,q.] is real-membered
proof end;
end;

registration
let p, q be Real;
cluster [.p,q.] -> real-membered ;
coherence
[.p,q.] is real-membered
proof end;
end;

:: from LIMFUNC1,2008.06.13, A.T.
theorem :: XXREAL_1:229
for s being ExtReal holds ].-infty,s.[ = { g where g is Real : g < s }
proof end;

theorem :: XXREAL_1:230
for s being ExtReal holds ].s,+infty.[ = { g where g is Real : s < g }
proof end;

theorem :: XXREAL_1:231
for s being Real holds ].-infty,s.] = { g where g is Real : g <= s }
proof end;

theorem :: XXREAL_1:232
for s being Real holds [.s,+infty.[ = { g where g is Real : s <= g }
proof end;

theorem :: XXREAL_1:233
for u being ExtReal
for x being Real holds
( x in ].-infty,u.[ iff x < u )
proof end;

theorem :: XXREAL_1:234
for u being ExtReal
for x being Real holds
( x in ].-infty,u.] iff x <= u )
proof end;

theorem :: XXREAL_1:235
for u being ExtReal
for x being Real holds
( x in ].u,+infty.[ iff u < x )
proof end;

theorem :: XXREAL_1:236
for u being ExtReal
for x being Real holds
( x in [.u,+infty.[ iff u <= x )
proof end;

theorem :: XXREAL_1:237
for p, r, s being ExtReal st p <= r holds
[.r,s.] c= [.p,+infty.]
proof end;

theorem :: XXREAL_1:238
for p, r, s being ExtReal st p <= r holds
[.r,s.[ c= [.p,+infty.]
proof end;

theorem :: XXREAL_1:239
for p, r, s being ExtReal st p <= r holds
].r,s.] c= [.p,+infty.]
proof end;

theorem :: XXREAL_1:240
for p, r, s being ExtReal st p <= r holds
].r,s.[ c= [.p,+infty.]
proof end;

theorem :: XXREAL_1:241
for p, r, s being ExtReal st p <= r holds
[.r,s.[ c= [.p,+infty.[
proof end;

theorem :: XXREAL_1:242
for p, r, s being ExtReal st p < r holds
[.r,s.] c= ].p,+infty.] by Th39, XXREAL_0:3;

theorem :: XXREAL_1:243
for p, r, s being ExtReal st p < r holds
[.r,s.[ c= ].p,+infty.] by Th40, XXREAL_0:3;

theorem :: XXREAL_1:244
for p, r, s being ExtReal st p <= r holds
].r,s.[ c= ].p,+infty.]
proof end;

theorem :: XXREAL_1:245
for p, r, s being ExtReal st p <= r holds
].r,s.] c= ].p,+infty.]
proof end;

theorem :: XXREAL_1:246
for p, r, s being ExtReal st p <= r holds
].r,s.[ c= [.p,+infty.[
proof end;

theorem :: XXREAL_1:247
for p, r, s being ExtReal st p <= r holds
].r,s.[ c= ].p,+infty.[
proof end;

theorem :: XXREAL_1:248
for p, r, s being ExtReal st p < r holds
[.r,s.[ c= ].p,+infty.[ by Th48, XXREAL_0:3;

theorem :: XXREAL_1:249
for p, r being ExtReal
for s being Real st p < r holds
[.r,s.] c= ].p,+infty.[
proof end;

theorem :: XXREAL_1:250
for p, r being ExtReal
for s being Real st p <= r holds
].r,s.] c= ].p,+infty.[
proof end;

theorem :: XXREAL_1:251
for p, r being ExtReal
for s being Real st p <= r holds
[.r,s.] c= [.p,+infty.[
proof end;

theorem :: XXREAL_1:252
for p, r being ExtReal
for s being Real st p <= r holds
].r,s.] c= [.p,+infty.[
proof end;

theorem :: XXREAL_1:253
for q, r, s being ExtReal st s <= q holds
[.r,s.] c= [.-infty,q.]
proof end;

theorem :: XXREAL_1:254
for q, r, s being ExtReal st s <= q holds
[.r,s.[ c= [.-infty,q.]
proof end;

theorem :: XXREAL_1:255
for q, r, s being ExtReal st s <= q holds
].r,s.] c= [.-infty,q.]
proof end;

theorem :: XXREAL_1:256
for q, r, s being ExtReal st s <= q holds
].r,s.[ c= [.-infty,q.]
proof end;

theorem :: XXREAL_1:257
for q, r, s being ExtReal st s <= q holds
[.r,s.[ c= [.-infty,q.[
proof end;

theorem :: XXREAL_1:258
for q, r, s being ExtReal st s <= q holds
].r,s.[ c= ].-infty,q.]
proof end;

theorem :: XXREAL_1:259
for q, r, s being ExtReal st s <= q holds
].r,s.] c= ].-infty,q.]
proof end;

theorem :: XXREAL_1:260
for q, r, s being ExtReal st s < q holds
[.r,s.] c= [.-infty,q.[ by Th43, XXREAL_0:5;

theorem :: XXREAL_1:261
for q, r, s being ExtReal st s < q holds
].r,s.] c= [.-infty,q.[ by Th44, XXREAL_0:5;

theorem :: XXREAL_1:262
for q, r, s being ExtReal st s <= q holds
].r,s.[ c= [.-infty,q.[
proof end;

theorem :: XXREAL_1:263
for q, r, s being ExtReal st s <= q holds
].r,s.[ c= ].-infty,q.[
proof end;

theorem :: XXREAL_1:264
for q, r, s being ExtReal st s < q holds
].r,s.] c= ].-infty,q.[ by Th49, XXREAL_0:5;

theorem :: XXREAL_1:265
for q, s being ExtReal
for r being Real st s <= q holds
[.r,s.] c= ].-infty,q.]
proof end;

theorem :: XXREAL_1:266
for q, s being ExtReal
for r being Real st s <= q holds
[.r,s.[ c= ].-infty,q.]
proof end;

theorem :: XXREAL_1:267
for q, s being ExtReal
for r being Real st s < q holds
[.r,s.] c= ].-infty,q.[
proof end;

theorem :: XXREAL_1:268
for q, s being ExtReal
for r being Real st s <= q holds
[.r,s.[ c= ].-infty,q.[
proof end;

theorem :: XXREAL_1:269
for a, b being ExtReal holds ].-infty,b.[ /\ ].a,+infty.[ = ].a,b.[
proof end;

theorem :: XXREAL_1:270
for p being ExtReal
for b being Real holds ].-infty,b.] /\ ].p,+infty.[ = ].p,b.]
proof end;

theorem :: XXREAL_1:271
for p being ExtReal
for a being Real holds ].-infty,p.[ /\ [.a,+infty.[ = [.a,p.[
proof end;

theorem :: XXREAL_1:272
for a, b being Real holds ].-infty,a.] /\ [.b,+infty.[ = [.b,a.]
proof end;

theorem :: XXREAL_1:273
for p, q, r, s being ExtReal st s <= p holds
[.r,s.[ misses ].p,q.[
proof end;

theorem :: XXREAL_1:274
for p, q, r, s being ExtReal st s <= p holds
[.r,s.[ misses ].p,q.]
proof end;

theorem :: XXREAL_1:275
for p, q, r, s being ExtReal st s <= p holds
].r,s.[ misses ].p,q.[
proof end;

theorem :: XXREAL_1:276
for p, q, r, s being ExtReal st s <= p holds
].r,s.[ misses ].p,q.]
proof end;

theorem :: XXREAL_1:277
for p, q, r, s being ExtReal st s < p holds
[.r,s.] misses [.p,q.[
proof end;

theorem :: XXREAL_1:278
for p, q, r, s being ExtReal st s < p holds
[.r,s.] misses [.p,q.]
proof end;

theorem :: XXREAL_1:279
for p, q, r, s being ExtReal st s < p holds
].r,s.] misses [.p,q.[
proof end;

theorem :: XXREAL_1:280
for p, q, r, s being ExtReal st s < p holds
].r,s.] misses [.p,q.]
proof end;

theorem :: XXREAL_1:281
for s, t being ExtReal holds [.-infty,t.] \ [.-infty,s.] = ].s,t.] by Th182, XXREAL_0:5;

theorem :: XXREAL_1:282
for s, t being ExtReal holds [.-infty,t.[ \ [.-infty,s.] = ].s,t.[ by Th183, XXREAL_0:5;

theorem :: XXREAL_1:283
for s, t being ExtReal holds [.-infty,t.] \ [.-infty,s.] = ].s,t.] by Th186, XXREAL_0:5;

theorem :: XXREAL_1:284
for r, s being ExtReal holds [.r,+infty.] \ [.s,+infty.] = [.r,s.[ by Th190, XXREAL_0:3;

theorem :: XXREAL_1:285
for r, s being ExtReal holds ].r,+infty.] \ [.s,+infty.] = ].r,s.[ by Th191, XXREAL_0:3;

theorem :: XXREAL_1:286
for t being ExtReal
for s being Real holds [.-infty,t.] \ [.-infty,s.[ = [.s,t.]
proof end;

theorem :: XXREAL_1:287
for t being ExtReal
for s being Real holds [.-infty,t.[ \ [.-infty,s.[ = [.s,t.[
proof end;

theorem :: XXREAL_1:288
for t being ExtReal
for s being Real holds ].-infty,t.[ \ ].-infty,s.] = ].s,t.[
proof end;

theorem :: XXREAL_1:289
for t being ExtReal
for s being Real holds ].-infty,t.] \ ].-infty,s.[ = [.s,t.]
proof end;

theorem :: XXREAL_1:290
for t being ExtReal
for s being Real holds ].-infty,t.[ \ ].-infty,s.[ = [.s,t.[
proof end;

theorem :: XXREAL_1:291
for r being ExtReal
for s being Real holds [.r,+infty.] \ ].s,+infty.] = [.r,s.]
proof end;

theorem :: XXREAL_1:292
for r being ExtReal
for s being Real holds ].r,+infty.] \ ].s,+infty.] = ].r,s.]
proof end;

theorem :: XXREAL_1:293
for r being ExtReal
for s being Real holds [.r,+infty.[ \ [.s,+infty.[ = [.r,s.[
proof end;

theorem :: XXREAL_1:294
for r being ExtReal
for s being Real holds ].r,+infty.[ \ [.s,+infty.[ = ].r,s.[
proof end;

theorem :: XXREAL_1:295
for r being ExtReal
for s being Real holds [.r,+infty.[ \ ].s,+infty.[ = [.r,s.]
proof end;

theorem :: XXREAL_1:296
for r being ExtReal
for s being Real holds ].r,+infty.[ \ ].s,+infty.[ = ].r,s.]
proof end;

theorem Th297: :: XXREAL_1:297
for p, q, r, s being ExtReal st r < s & p < q holds
].r,q.[ \ ].p,s.[ = ].r,p.] \/ [.s,q.[
proof end;

theorem Th298: :: XXREAL_1:298
for p, q, r, s being ExtReal st r <= s & p < q holds
[.r,q.[ \ ].p,s.[ = [.r,p.] \/ [.s,q.[
proof end;

theorem Th299: :: XXREAL_1:299
for p, q, r, s being ExtReal st r < s & p <= q holds
].r,q.] \ ].p,s.[ = ].r,p.] \/ [.s,q.]
proof end;

theorem Th300: :: XXREAL_1:300
for p, q, r, s being ExtReal st r <= s & p <= q holds
[.r,q.] \ ].p,s.[ = [.r,p.] \/ [.s,q.]
proof end;

theorem Th301: :: XXREAL_1:301
for p, q, r, s being ExtReal st r < s & p <= q holds
].r,q.[ \ [.p,s.[ = ].r,p.[ \/ [.s,q.[
proof end;

theorem Th302: :: XXREAL_1:302
for p, q, r, s being ExtReal st r <= s & p <= q holds
[.r,q.[ \ [.p,s.[ = [.r,p.[ \/ [.s,q.[
proof end;

theorem Th303: :: XXREAL_1:303
for p, q, r, s being ExtReal st r < s & p <= q holds
].r,q.] \ [.p,s.[ = ].r,p.[ \/ [.s,q.]
proof end;

theorem Th304: :: XXREAL_1:304
for p, q, r, s being ExtReal st r <= s & p <= q holds
[.r,q.] \ [.p,s.[ = [.r,p.[ \/ [.s,q.]
proof end;

theorem Th305: :: XXREAL_1:305
for p, q, r, s being ExtReal st r < s & p < q holds
].r,q.[ \ ].p,s.] = ].r,p.] \/ ].s,q.[
proof end;

theorem Th306: :: XXREAL_1:306
for p, q, r, s being ExtReal st r <= s & p < q holds
[.r,q.[ \ ].p,s.] = [.r,p.] \/ ].s,q.[
proof end;

theorem Th307: :: XXREAL_1:307
for p, q, r, s being ExtReal st r < s & p <= q holds
].r,q.] \ ].p,s.] = ].r,p.] \/ ].s,q.]
proof end;

theorem Th308: :: XXREAL_1:308
for p, q, r, s being ExtReal st r <= s & p <= q holds
[.r,q.] \ ].p,s.] = [.r,p.] \/ ].s,q.]
proof end;

theorem Th309: :: XXREAL_1:309
for p, q, r, s being ExtReal st r <= s & p <= q holds
].r,q.[ \ [.p,s.] = ].r,p.[ \/ ].s,q.[
proof end;

theorem Th310: :: XXREAL_1:310
for p, q, r, s being ExtReal st r <= s & p <= q holds
[.r,q.[ \ [.p,s.] = [.r,p.[ \/ ].s,q.[
proof end;

theorem Th311: :: XXREAL_1:311
for p, q, r, s being ExtReal st r < s & p <= q holds
].r,q.] \ [.p,s.] = ].r,p.[ \/ ].s,q.]
proof end;

theorem Th312: :: XXREAL_1:312
for p, q, r, s being ExtReal st r <= s & p <= q holds
[.r,q.] \ [.p,s.] = [.r,p.[ \/ ].s,q.]
proof end;

theorem Th313: :: XXREAL_1:313
for p, q, r being ExtReal st r <= p & p <= q holds
].r,q.[ \ {p} = ].r,p.[ \/ ].p,q.[
proof end;

theorem Th314: :: XXREAL_1:314
for p, q, r being ExtReal st r <= p & p <= q holds
[.r,q.[ \ {p} = [.r,p.[ \/ ].p,q.[
proof end;

theorem Th315: :: XXREAL_1:315
for p, q, r being ExtReal st r < p & p <= q holds
].r,q.] \ {p} = ].r,p.[ \/ ].p,q.]
proof end;

theorem Th316: :: XXREAL_1:316
for p, q, r being ExtReal st r <= p & p <= q holds
[.r,q.] \ {p} = [.r,p.[ \/ ].p,q.]
proof end;

theorem Th317: :: XXREAL_1:317
for p, q, r being ExtReal st r < q & p <= q holds
].r,q.] \ ].p,q.[ = ].r,p.] \/ {q}
proof end;

theorem Th318: :: XXREAL_1:318
for p, q, r being ExtReal st r <= q & p <= q holds
[.r,q.] \ ].p,q.[ = [.r,p.] \/ {q}
proof end;

theorem Th319: :: XXREAL_1:319
for p, q, r being ExtReal st r < q & p <= q holds
].r,q.] \ [.p,q.[ = ].r,p.[ \/ {q}
proof end;

theorem Th320: :: XXREAL_1:320
for p, q, r being ExtReal st r <= q & p <= q holds
[.r,q.] \ [.p,q.[ = [.r,p.[ \/ {q}
proof end;

theorem Th321: :: XXREAL_1:321
for p, q, s being ExtReal st p <= s & p < q holds
[.p,q.[ \ ].p,s.[ = {p} \/ [.s,q.[
proof end;

theorem Th322: :: XXREAL_1:322
for p, q, s being ExtReal st p <= s & p <= q holds
[.p,q.] \ ].p,s.[ = {p} \/ [.s,q.]
proof end;

theorem Th323: :: XXREAL_1:323
for p, q, s being ExtReal st p <= s & p < q holds
[.p,q.[ \ ].p,s.] = {p} \/ ].s,q.[
proof end;

theorem Th324: :: XXREAL_1:324
for p, q, s being ExtReal st p <= s & p <= q holds
[.p,q.] \ ].p,s.] = {p} \/ ].s,q.]
proof end;

theorem Th325: :: XXREAL_1:325
for p, q, s being ExtReal st p < q holds
[.-infty,q.[ \ ].p,s.[ = [.-infty,p.] \/ [.s,q.[ by Th298, XXREAL_0:5;

theorem Th326: :: XXREAL_1:326
for p, q, s being ExtReal st p <= q holds
[.-infty,q.] \ ].p,s.[ = [.-infty,p.] \/ [.s,q.]
proof end;

theorem Th327: :: XXREAL_1:327
for p, q, s being ExtReal st p <= q holds
[.-infty,q.[ \ [.p,s.[ = [.-infty,p.[ \/ [.s,q.[
proof end;

theorem Th328: :: XXREAL_1:328
for p, q, s being ExtReal st p <= q holds
[.-infty,q.] \ [.p,s.[ = [.-infty,p.[ \/ [.s,q.]
proof end;

theorem Th329: :: XXREAL_1:329
for p, q, s being ExtReal st p < q holds
[.-infty,q.[ \ ].p,s.] = [.-infty,p.] \/ ].s,q.[ by Th306, XXREAL_0:5;

theorem Th330: :: XXREAL_1:330
for p, q, s being ExtReal st p <= q holds
[.-infty,q.] \ ].p,s.] = [.-infty,p.] \/ ].s,q.]
proof end;

theorem Th331: :: XXREAL_1:331
for p, q, s being ExtReal st p <= q holds
[.-infty,q.[ \ [.p,s.] = [.-infty,p.[ \/ ].s,q.[
proof end;

theorem Th332: :: XXREAL_1:332
for p, q, s being ExtReal st p <= q holds
[.-infty,q.] \ [.p,s.] = [.-infty,p.[ \/ ].s,q.]
proof end;

theorem Th333: :: XXREAL_1:333
for p, q being ExtReal
for s being Real st p < q holds
].-infty,q.[ \ ].p,s.[ = ].-infty,p.] \/ [.s,q.[
proof end;

theorem Th334: :: XXREAL_1:334
for p, q being ExtReal
for s being Real st p <= q holds
].-infty,q.] \ ].p,s.[ = ].-infty,p.] \/ [.s,q.]
proof end;

theorem Th335: :: XXREAL_1:335
for p, q being ExtReal
for s being Real st p <= q holds
].-infty,q.[ \ [.p,s.[ = ].-infty,p.[ \/ [.s,q.[
proof end;

theorem Th336: :: XXREAL_1:336
for p, q being ExtReal
for s being Real st p <= q holds
].-infty,q.] \ [.p,s.[ = ].-infty,p.[ \/ [.s,q.]
proof end;

theorem Th337: :: XXREAL_1:337
for p, q being ExtReal
for s being Real st p < q holds
].-infty,q.[ \ ].p,s.] = ].-infty,p.] \/ ].s,q.[
proof end;

theorem Th338: :: XXREAL_1:338
for p, q being ExtReal
for s being Real st p <= q holds
].-infty,q.] \ ].p,s.] = ].-infty,p.] \/ ].s,q.]
proof end;

theorem Th339: :: XXREAL_1:339
for p, q, s being ExtReal st p <= q holds
].-infty,q.[ \ [.p,s.] = ].-infty,p.[ \/ ].s,q.[
proof end;

theorem Th340: :: XXREAL_1:340
for p, q being ExtReal
for s being Real st p <= q holds
].-infty,q.] \ [.p,s.] = ].-infty,p.[ \/ ].s,q.]
proof end;

theorem Th341: :: XXREAL_1:341
for p, q being ExtReal st p <= q holds
[.-infty,q.[ \ {p} = [.-infty,p.[ \/ ].p,q.[
proof end;

theorem Th342: :: XXREAL_1:342
for p, q being ExtReal st p <= q holds
[.-infty,q.] \ {p} = [.-infty,p.[ \/ ].p,q.]
proof end;

theorem :: XXREAL_1:343
for p, q being ExtReal st p <= q holds
[.-infty,q.] \ ].p,q.[ = [.-infty,p.] \/ {q}
proof end;

theorem :: XXREAL_1:344
for p, q being ExtReal st p <= q holds
[.-infty,q.] \ [.p,q.[ = [.-infty,p.[ \/ {q}
proof end;

theorem :: XXREAL_1:345
for q, s being ExtReal holds [.-infty,q.] \ ].-infty,s.[ = {-infty} \/ [.s,q.]
proof end;

theorem :: XXREAL_1:346
for q, s being ExtReal holds [.-infty,q.] \ ].-infty,s.] = {-infty} \/ ].s,q.]
proof end;

theorem :: XXREAL_1:347
for s being ExtReal
for q being Real holds [.-infty,q.[ \ ].-infty,s.[ = {-infty} \/ [.s,q.[
proof end;

theorem :: XXREAL_1:348
for s being ExtReal
for q being Real holds [.-infty,q.[ \ ].-infty,s.] = {-infty} \/ ].s,q.[
proof end;

theorem Th349: :: XXREAL_1:349
for p, q being ExtReal st p <= q holds
].-infty,q.[ \ {p} = ].-infty,p.[ \/ ].p,q.[
proof end;

theorem Th350: :: XXREAL_1:350
for q being ExtReal
for p being Real st p <= q holds
].-infty,q.] \ {p} = ].-infty,p.[ \/ ].p,q.]
proof end;

theorem :: XXREAL_1:351
for p being ExtReal
for q being Real st p <= q holds
].-infty,q.] \ ].p,q.[ = ].-infty,p.] \/ {q}
proof end;

theorem :: XXREAL_1:352
for p being ExtReal
for q being Real st p <= q holds
].-infty,q.] \ [.p,q.[ = ].-infty,p.[ \/ {q}
proof end;

theorem :: XXREAL_1:353
for p, r, s being ExtReal st r < s holds
].r,+infty.] \ ].p,s.[ = ].r,p.] \/ [.s,+infty.] by Th299, XXREAL_0:3;

theorem :: XXREAL_1:354
for p, r, s being ExtReal st r <= s holds
[.r,+infty.] \ ].p,s.[ = [.r,p.] \/ [.s,+infty.]
proof end;

theorem :: XXREAL_1:355
for p, r, s being ExtReal st r < s holds
].r,+infty.[ \ [.p,s.[ = ].r,p.[ \/ [.s,+infty.[ by Th301, XXREAL_0:3;

theorem :: XXREAL_1:356
for p, r, s being ExtReal st r <= s holds
[.r,+infty.[ \ [.p,s.[ = [.r,p.[ \/ [.s,+infty.[
proof end;

theorem :: XXREAL_1:357
for p, r, s being ExtReal st r < s holds
].r,+infty.] \ [.p,s.[ = ].r,p.[ \/ [.s,+infty.] by Th303, XXREAL_0:3;

theorem :: XXREAL_1:358
for p, r, s being ExtReal st r <= s holds
[.r,+infty.] \ [.p,s.[ = [.r,p.[ \/ [.s,+infty.]
proof end;

theorem :: XXREAL_1:359
for p, r, s being ExtReal st r < s holds
].r,+infty.] \ ].p,s.] = ].r,p.] \/ ].s,+infty.] by Th307, XXREAL_0:3;

theorem :: XXREAL_1:360
for p, r, s being ExtReal st r <= s holds
[.r,+infty.] \ ].p,s.] = [.r,p.] \/ ].s,+infty.]
proof end;

theorem :: XXREAL_1:361
for p, r, s being ExtReal st r <= s holds
].r,+infty.[ \ [.p,s.] = ].r,p.[ \/ ].s,+infty.[
proof end;

theorem :: XXREAL_1:362
for p, r, s being ExtReal st r <= s holds
[.r,+infty.[ \ [.p,s.] = [.r,p.[ \/ ].s,+infty.[
proof end;

theorem :: XXREAL_1:363
for p, r, s being ExtReal st r < s holds
].r,+infty.] \ [.p,s.] = ].r,p.[ \/ ].s,+infty.] by Th311, XXREAL_0:3;

theorem :: XXREAL_1:364
for p, r, s being ExtReal st r <= s holds
[.r,+infty.] \ [.p,s.] = [.r,p.[ \/ ].s,+infty.]
proof end;

theorem :: XXREAL_1:365
for p, r being ExtReal st r <= p holds
].r,+infty.[ \ {p} = ].r,p.[ \/ ].p,+infty.[
proof end;

theorem :: XXREAL_1:366
for p, r being ExtReal st r <= p holds
[.r,+infty.[ \ {p} = [.r,p.[ \/ ].p,+infty.[
proof end;

theorem :: XXREAL_1:367
for p, r being ExtReal st r < p holds
].r,+infty.] \ {p} = ].r,p.[ \/ ].p,+infty.] by Th315, XXREAL_0:3;

theorem :: XXREAL_1:368
for p, r being ExtReal st r <= p holds
[.r,+infty.] \ {p} = [.r,p.[ \/ ].p,+infty.]
proof end;

theorem :: XXREAL_1:369
for p, r being ExtReal holds [.r,+infty.] \ ].p,+infty.[ = [.r,p.] \/ {+infty}
proof end;

theorem :: XXREAL_1:370
for p, r being ExtReal holds [.r,+infty.] \ [.p,+infty.[ = [.r,p.[ \/ {+infty}
proof end;

theorem :: XXREAL_1:371
for p being ExtReal
for r being Real holds ].r,+infty.] \ ].p,+infty.[ = ].r,p.] \/ {+infty}
proof end;

theorem :: XXREAL_1:372
for p being ExtReal
for r being Real holds ].r,+infty.] \ [.p,+infty.[ = ].r,p.[ \/ {+infty}
proof end;

theorem :: XXREAL_1:373
for p, s being ExtReal st p <= s holds
[.p,+infty.] \ ].p,s.[ = {p} \/ [.s,+infty.]
proof end;

theorem :: XXREAL_1:374
for p, s being ExtReal st p <= s holds
[.p,+infty.] \ ].p,s.] = {p} \/ ].s,+infty.]
proof end;

theorem :: XXREAL_1:375
for p, s being ExtReal holds [.-infty,+infty.] \ ].p,s.[ = [.-infty,p.] \/ [.s,+infty.] by Th326, XXREAL_0:3;

theorem :: XXREAL_1:376
for p, s being ExtReal holds [.-infty,+infty.[ \ [.p,s.[ = [.-infty,p.[ \/ [.s,+infty.[ by Th327, XXREAL_0:3;

theorem :: XXREAL_1:377
for p, s being ExtReal holds [.-infty,+infty.] \ [.p,s.[ = [.-infty,p.[ \/ [.s,+infty.] by Th328, XXREAL_0:3;

theorem :: XXREAL_1:378
for p, s being ExtReal holds [.-infty,+infty.] \ ].p,s.] = [.-infty,p.] \/ ].s,+infty.] by Th330, XXREAL_0:3;

theorem :: XXREAL_1:379
for p, s being ExtReal holds [.-infty,+infty.[ \ [.p,s.] = [.-infty,p.[ \/ ].s,+infty.[ by Th331, XXREAL_0:3;

theorem :: XXREAL_1:380
for p, s being ExtReal holds [.-infty,+infty.] \ [.p,s.] = [.-infty,p.[ \/ ].s,+infty.] by Th332, XXREAL_0:3;

theorem :: XXREAL_1:381
for p being ExtReal
for s being Real holds ].-infty,+infty.] \ ].p,s.[ = ].-infty,p.] \/ [.s,+infty.] by Th334, XXREAL_0:3;

theorem :: XXREAL_1:382
for p being ExtReal
for s being Real holds REAL \ [.p,s.[ = ].-infty,p.[ \/ [.s,+infty.[ by Th224, Th335, XXREAL_0:3;

theorem :: XXREAL_1:383
for p being ExtReal
for s being Real holds ].-infty,+infty.] \ [.p,s.[ = ].-infty,p.[ \/ [.s,+infty.] by Th336, XXREAL_0:3;

theorem :: XXREAL_1:384
for p being ExtReal
for s being Real holds ].-infty,+infty.] \ ].p,s.] = ].-infty,p.] \/ ].s,+infty.] by Th338, XXREAL_0:3;

theorem :: XXREAL_1:385
for p, s being ExtReal holds REAL \ [.p,s.] = ].-infty,p.[ \/ ].s,+infty.[ by Th224, Th339, XXREAL_0:3;

theorem :: XXREAL_1:386
for p being ExtReal
for s being Real holds ].-infty,+infty.] \ [.p,s.] = ].-infty,p.[ \/ ].s,+infty.] by Th340, XXREAL_0:3;

theorem :: XXREAL_1:387
for p being ExtReal holds [.-infty,+infty.[ \ {p} = [.-infty,p.[ \/ ].p,+infty.[ by Th341, XXREAL_0:3;

theorem :: XXREAL_1:388
for p being ExtReal holds [.-infty,+infty.] \ {p} = [.-infty,p.[ \/ ].p,+infty.] by Th342, XXREAL_0:3;

theorem :: XXREAL_1:389
for p being ExtReal holds REAL \ {p} = ].-infty,p.[ \/ ].p,+infty.[ by Th224, Th349, XXREAL_0:3;

theorem :: XXREAL_1:390
for p being Real holds ].-infty,+infty.] \ {p} = ].-infty,p.[ \/ ].p,+infty.] by Th350, XXREAL_0:3;

theorem :: XXREAL_1:391
for r, s being ExtReal
for p being Real st r < s holds
].r,+infty.[ \ ].p,s.[ = ].r,p.] \/ [.s,+infty.[
proof end;

theorem :: XXREAL_1:392
for r, s being ExtReal
for p being Real st r <= s holds
[.r,+infty.[ \ ].p,s.[ = [.r,p.] \/ [.s,+infty.[
proof end;

theorem :: XXREAL_1:393
for r, s being ExtReal
for p being Real st r < s holds
].r,+infty.[ \ ].p,s.] = ].r,p.] \/ ].s,+infty.[
proof end;

theorem :: XXREAL_1:394
for r, s being ExtReal
for p being Real st r <= s holds
[.r,+infty.[ \ ].p,s.] = [.r,p.] \/ ].s,+infty.[
proof end;

theorem :: XXREAL_1:395
for s being ExtReal
for p being Real st p <= s holds
[.p,+infty.[ \ ].p,s.] = {p} \/ ].s,+infty.[
proof end;

theorem :: XXREAL_1:396
for s being ExtReal
for p being Real holds [.-infty,+infty.[ \ ].p,s.[ = [.-infty,p.] \/ [.s,+infty.[
proof end;

theorem :: XXREAL_1:397
for s being ExtReal
for p being Real holds [.-infty,+infty.[ \ ].p,s.] = [.-infty,p.] \/ ].s,+infty.[
proof end;

theorem :: XXREAL_1:398
for s, p being Real holds REAL \ ].p,s.[ = ].-infty,p.] \/ [.s,+infty.[
proof end;

theorem :: XXREAL_1:399
for s, p being Real holds REAL \ ].p,s.] = ].-infty,p.] \/ ].s,+infty.[
proof end;

theorem :: XXREAL_1:400
for s being ExtReal
for p being Real st p <= s holds
[.p,+infty.[ \ ].p,s.[ = {p} \/ [.s,+infty.[
proof end;

theorem Th401: :: XXREAL_1:401
for r, s being ExtReal st r < s holds
[.r,s.] \ [.r,s.[ = {s}
proof end;

theorem Th402: :: XXREAL_1:402
for r, s being ExtReal st r < s holds
].r,s.] \ ].r,s.[ = {s}
proof end;

theorem Th403: :: XXREAL_1:403
for r, t being ExtReal st r < t holds
[.r,t.] \ ].r,t.] = {r}
proof end;

theorem Th404: :: XXREAL_1:404
for r, t being ExtReal st r < t holds
[.r,t.[ \ ].r,t.[ = {r}
proof end;

theorem :: XXREAL_1:405
for s being Real holds [.-infty,s.] \ [.-infty,s.[ = {s}
proof end;

theorem :: XXREAL_1:406
for s being Real holds ].-infty,s.] \ ].-infty,s.[ = {s}
proof end;

theorem :: XXREAL_1:407
for s being Real holds [.-infty,s.] \ ].-infty,s.] = {-infty}
proof end;

theorem :: XXREAL_1:408
for s being Real holds [.-infty,s.[ \ ].-infty,s.[ = {-infty}
proof end;

theorem :: XXREAL_1:409
for s being Real holds [.s,+infty.] \ [.s,+infty.[ = {+infty}
proof end;

theorem :: XXREAL_1:410
for s being Real holds ].s,+infty.] \ ].s,+infty.[ = {+infty}
proof end;

theorem :: XXREAL_1:411
for s being Real holds [.s,+infty.] \ ].s,+infty.] = {s}
proof end;

theorem :: XXREAL_1:412
for s being Real holds [.s,+infty.[ \ ].s,+infty.[ = {s}
proof end;

:: analogous to Th165
theorem :: XXREAL_1:413
for r, s, t being ExtReal st r <= s & s < t holds
[.r,s.] \/ [.s,t.[ = [.r,t.[
proof end;

theorem :: XXREAL_1:414
for r, s, t being ExtReal st r < s & s <= t holds
].r,s.] \/ [.s,t.] = ].r,t.]
proof end;

theorem :: XXREAL_1:415
for r, s, t being ExtReal st r < s & s < t holds
].r,s.] \/ [.s,t.[ = ].r,t.[
proof end;

:: analogous to Th138
theorem :: XXREAL_1:416
for r, s, t being ExtReal st r <= s & s < t holds
[.r,s.] /\ [.s,t.[ = {s}
proof end;

theorem :: XXREAL_1:417
for r, s, t being ExtReal st r < s & s <= t holds
].r,s.] /\ [.s,t.] = {s}
proof end;

theorem :: XXREAL_1:418
for r, s, t being ExtReal st r <= s & s <= t holds
[.r,s.] /\ [.s,t.] = {s}
proof end;

:: special cases of Th128-Th132
theorem :: XXREAL_1:419
for s being ExtReal holds [.-infty,s.] = ].-infty,s.[ \/ {-infty,s} by Th128, XXREAL_0:5;

theorem :: XXREAL_1:420
for s being ExtReal holds [.-infty,s.] = [.-infty,s.[ \/ {s} by Th129, XXREAL_0:5;

theorem :: XXREAL_1:421
for s being ExtReal holds [.-infty,s.] = {-infty} \/ ].-infty,s.] by Th130, XXREAL_0:5;

theorem :: XXREAL_1:422
for s being Real holds [.-infty,s.[ = {-infty} \/ ].-infty,s.[
proof end;

theorem :: XXREAL_1:423
for s being Real holds ].-infty,s.] = ].-infty,s.[ \/ {s}
proof end;

theorem :: XXREAL_1:424
for r being ExtReal holds [.r,+infty.] = ].r,+infty.[ \/ {r,+infty} by Th128, XXREAL_0:3;

theorem :: XXREAL_1:425
for r being ExtReal holds [.r,+infty.] = [.r,+infty.[ \/ {+infty} by Th129, XXREAL_0:3;

theorem :: XXREAL_1:426
for r being ExtReal holds [.r,+infty.] = {r} \/ ].r,+infty.] by Th130, XXREAL_0:3;

theorem :: XXREAL_1:427
for r being Real holds [.r,+infty.[ = {r} \/ ].r,+infty.[
proof end;

theorem :: XXREAL_1:428
for r being Real holds ].r,+infty.] = ].r,+infty.[ \/ {+infty}
proof end;