Loading [MathJax]/extensions/tex2jax.js

:: 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{ P₁[ object ], P₂[ object ] } :

ex s being ExtReal st
( ( for r being ExtReal st P₁[r] holds
r <= s ) & ( for r being ExtReal st P₂[r] holds
s <= r ) )

provided

A1: for r, s being ExtReal st P₁[r] & P₂[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;