:: MEASURE5 semantic presentation

theorem Th1: :: MEASURE5:1
for b1, b2 being R_eal st b1 <> -infty & b1 <> +infty & b1 <=' b2 holds
0. <=' b2 - b1
proof end;

theorem Th2: :: MEASURE5:2
for b1, b2 being R_eal st ( not b1 = -infty or not b2 = -infty ) & ( not b1 = +infty or not b2 = +infty ) & b1 <=' b2 holds
0. <=' b2 - b1
proof end;

theorem Th3: :: MEASURE5:3
canceled;

theorem Th4: :: MEASURE5:4
canceled;

theorem Th5: :: MEASURE5:5
canceled;

theorem Th6: :: MEASURE5:6
canceled;

theorem Th7: :: MEASURE5:7
canceled;

theorem Th8: :: MEASURE5:8
for b1, b2, b3 being R_eal st b2 <> -infty & b2 <> +infty & ( not b1 = -infty or not b3 = -infty ) & ( not b1 = +infty or not b3 = +infty ) holds
(b3 - b2) + (b2 - b1) = b3 - b1
proof end;

theorem Th9: :: MEASURE5:9
for b1, b2 being R_eal holds
( inf {b1,b2} <=' b1 & inf {b1,b2} <=' b2 & b1 <=' sup {b1,b2} & b2 <=' sup {b1,b2} )
proof end;

scheme :: MEASURE5:sch 1
s1{ P1[ set ] } :
for b1, b2 being Subset of REAL st ( for b3 being R_eal holds
( b3 in b1 iff P1[b3] ) ) & ( for b3 being R_eal holds
( b3 in b2 iff P1[b3] ) ) holds
b1 = b2
proof end;

definition
let c1, c2 be R_eal;
defpred S1[ R_eal] means ( c1 <=' a1 & a1 <=' c2 & a1 in REAL );
func [.c1,c2.] -> Subset of REAL means :Def1: :: MEASURE5:def 1
for b1 being R_eal holds
( b1 in a3 iff ( a1 <=' b1 & b1 <=' a2 & b1 in REAL ) );
existence
ex b1 being Subset of REAL st
for b2 being R_eal holds
( b2 in b1 iff ( c1 <=' b2 & b2 <=' c2 & b2 in REAL ) )
proof end;
uniqueness
for b1, b2 being Subset of REAL st ( for b3 being R_eal holds
( b3 in b1 iff ( c1 <=' b3 & b3 <=' c2 & b3 in REAL ) ) ) & ( for b3 being R_eal holds
( b3 in b2 iff ( c1 <=' b3 & b3 <=' c2 & b3 in REAL ) ) ) holds
b1 = b2
proof end;
defpred S2[ R_eal] means ( c1 <' a1 & a1 <' c2 & a1 in REAL );
func ].c1,c2.[ -> Subset of REAL means :Def2: :: MEASURE5:def 2
for b1 being R_eal holds
( b1 in a3 iff ( a1 <' b1 & b1 <' a2 & b1 in REAL ) );
existence
ex b1 being Subset of REAL st
for b2 being R_eal holds
( b2 in b1 iff ( c1 <' b2 & b2 <' c2 & b2 in REAL ) )
proof end;
uniqueness
for b1, b2 being Subset of REAL st ( for b3 being R_eal holds
( b3 in b1 iff ( c1 <' b3 & b3 <' c2 & b3 in REAL ) ) ) & ( for b3 being R_eal holds
( b3 in b2 iff ( c1 <' b3 & b3 <' c2 & b3 in REAL ) ) ) holds
b1 = b2
proof end;
defpred S3[ R_eal] means ( c1 <' a1 & a1 <=' c2 & a1 in REAL );
func ].c1,c2.] -> Subset of REAL means :Def3: :: MEASURE5:def 3
for b1 being R_eal holds
( b1 in a3 iff ( a1 <' b1 & b1 <=' a2 & b1 in REAL ) );
existence
ex b1 being Subset of REAL st
for b2 being R_eal holds
( b2 in b1 iff ( c1 <' b2 & b2 <=' c2 & b2 in REAL ) )
proof end;
uniqueness
for b1, b2 being Subset of REAL st ( for b3 being R_eal holds
( b3 in b1 iff ( c1 <' b3 & b3 <=' c2 & b3 in REAL ) ) ) & ( for b3 being R_eal holds
( b3 in b2 iff ( c1 <' b3 & b3 <=' c2 & b3 in REAL ) ) ) holds
b1 = b2
proof end;
defpred S4[ R_eal] means ( c1 <=' a1 & a1 <' c2 & a1 in REAL );
func [.c1,c2.[ -> Subset of REAL means :Def4: :: MEASURE5:def 4
for b1 being R_eal holds
( b1 in a3 iff ( a1 <=' b1 & b1 <' a2 & b1 in REAL ) );
existence
ex b1 being Subset of REAL st
for b2 being R_eal holds
( b2 in b1 iff ( c1 <=' b2 & b2 <' c2 & b2 in REAL ) )
proof end;
uniqueness
for b1, b2 being Subset of REAL st ( for b3 being R_eal holds
( b3 in b1 iff ( c1 <=' b3 & b3 <' c2 & b3 in REAL ) ) ) & ( for b3 being R_eal holds
( b3 in b2 iff ( c1 <=' b3 & b3 <' c2 & b3 in REAL ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines [. MEASURE5:def 1 :
for b1, b2 being R_eal
for b3 being Subset of REAL holds
( b3 = [.b1,b2.] iff for b4 being R_eal holds
( b4 in b3 iff ( b1 <=' b4 & b4 <=' b2 & b4 in REAL ) ) );

:: deftheorem Def2 defines ]. MEASURE5:def 2 :
for b1, b2 being R_eal
for b3 being Subset of REAL holds
( b3 = ].b1,b2.[ iff for b4 being R_eal holds
( b4 in b3 iff ( b1 <' b4 & b4 <' b2 & b4 in REAL ) ) );

:: deftheorem Def3 defines ]. MEASURE5:def 3 :
for b1, b2 being R_eal
for b3 being Subset of REAL holds
( b3 = ].b1,b2.] iff for b4 being R_eal holds
( b4 in b3 iff ( b1 <' b4 & b4 <=' b2 & b4 in REAL ) ) );

:: deftheorem Def4 defines [. MEASURE5:def 4 :
for b1, b2 being R_eal
for b3 being Subset of REAL holds
( b3 = [.b1,b2.[ iff for b4 being R_eal holds
( b4 in b3 iff ( b1 <=' b4 & b4 <' b2 & b4 in REAL ) ) );

definition
let c1 be Subset of REAL ;
attr a1 is open_interval means :Def5: :: MEASURE5:def 5
ex b1, b2 being R_eal st
( b1 <=' b2 & a1 = ].b1,b2.[ );
attr a1 is closed_interval means :Def6: :: MEASURE5:def 6
ex b1, b2 being R_eal st
( b1 <=' b2 & a1 = [.b1,b2.] );
end;

:: deftheorem Def5 defines open_interval MEASURE5:def 5 :
for b1 being Subset of REAL holds
( b1 is open_interval iff ex b2, b3 being R_eal st
( b2 <=' b3 & b1 = ].b2,b3.[ ) );

:: deftheorem Def6 defines closed_interval MEASURE5:def 6 :
for b1 being Subset of REAL holds
( b1 is closed_interval iff ex b2, b3 being R_eal st
( b2 <=' b3 & b1 = [.b2,b3.] ) );

registration
cluster open_interval Element of K40(REAL );
existence
ex b1 being Subset of REAL st b1 is open_interval
proof end;
cluster closed_interval Element of K40(REAL );
existence
ex b1 being Subset of REAL st b1 is closed_interval
proof end;
end;

definition
let c1 be Subset of REAL ;
attr a1 is right_open_interval means :Def7: :: MEASURE5:def 7
ex b1, b2 being R_eal st
( b1 <=' b2 & a1 = [.b1,b2.[ );
end;

:: deftheorem Def7 defines right_open_interval MEASURE5:def 7 :
for b1 being Subset of REAL holds
( b1 is right_open_interval iff ex b2, b3 being R_eal st
( b2 <=' b3 & b1 = [.b2,b3.[ ) );

notation
let c1 be Subset of REAL ;
synonym left_closed_interval c1 for right_open_interval c1;
end;

definition
let c1 be Subset of REAL ;
attr a1 is left_open_interval means :Def8: :: MEASURE5:def 8
ex b1, b2 being R_eal st
( b1 <=' b2 & a1 = ].b1,b2.] );
end;

:: deftheorem Def8 defines left_open_interval MEASURE5:def 8 :
for b1 being Subset of REAL holds
( b1 is left_open_interval iff ex b2, b3 being R_eal st
( b2 <=' b3 & b1 = ].b2,b3.] ) );

notation
let c1 be Subset of REAL ;
synonym right_closed_interval c1 for left_open_interval c1;
end;

registration
cluster right_open_interval Element of K40(REAL );
existence
ex b1 being Subset of REAL st b1 is right_open_interval
proof end;
cluster left_open_interval Element of K40(REAL );
existence
ex b1 being Subset of REAL st b1 is left_open_interval
proof end;
end;

definition
let c1 be Subset of REAL ;
attr a1 is interval means :Def9: :: MEASURE5:def 9
( a1 is open_interval or a1 is closed_interval or a1 is right_open_interval or a1 is left_open_interval );
end;

:: deftheorem Def9 defines interval MEASURE5:def 9 :
for b1 being Subset of REAL holds
( b1 is interval iff ( b1 is open_interval or b1 is closed_interval or b1 is right_open_interval or b1 is left_open_interval ) );

registration
cluster interval Element of K40(REAL );
existence
ex b1 being Subset of REAL st b1 is interval
proof end;
end;

definition
mode Interval is interval Subset of REAL ;
end;

registration
cluster open_interval -> interval Element of K40(REAL );
coherence
for b1 being Subset of REAL st b1 is open_interval holds
b1 is interval by Def9;
cluster closed_interval -> interval Element of K40(REAL );
coherence
for b1 being Subset of REAL st b1 is closed_interval holds
b1 is interval by Def9;
cluster right_open_interval -> interval Element of K40(REAL );
coherence
for b1 being Subset of REAL st b1 is right_open_interval holds
b1 is interval by Def9;
cluster left_open_interval -> interval Element of K40(REAL );
coherence
for b1 being Subset of REAL st b1 is left_open_interval holds
b1 is interval by Def9;
end;

theorem Th10: :: MEASURE5:10
canceled;

theorem Th11: :: MEASURE5:11
for b1 being set
for b2, b3 being R_eal st ( b1 in ].b2,b3.[ or b1 in [.b2,b3.] or b1 in [.b2,b3.[ or b1 in ].b2,b3.] ) holds
b1 is R_eal
proof end;

theorem Th12: :: MEASURE5:12
for b1, b2 being R_eal st b2 <' b1 holds
( ].b1,b2.[ = {} & [.b1,b2.] = {} & [.b1,b2.[ = {} & ].b1,b2.] = {} )
proof end;

theorem Th13: :: MEASURE5:13
for b1 being R_eal holds
( ].b1,b1.[ = {} & [.b1,b1.[ = {} & ].b1,b1.] = {} )
proof end;

theorem Th14: :: MEASURE5:14
for b1 being R_eal holds
( ( ( b1 = -infty or b1 = +infty ) implies [.b1,b1.] = {} ) & ( b1 <> -infty & b1 <> +infty implies [.b1,b1.] = {b1} ) )
proof end;

theorem Th15: :: MEASURE5:15
for b1, b2 being R_eal st b2 <=' b1 holds
( ].b1,b2.[ = {} & [.b1,b2.[ = {} & ].b1,b2.] = {} & [.b1,b2.] c= {b1} & [.b1,b2.] c= {b2} )
proof end;

theorem Th16: :: MEASURE5:16
for b1, b2, b3 being R_eal st b1 <' b2 & b2 <' b3 holds
b2 in REAL
proof end;

theorem Th17: :: MEASURE5:17
for b1, b2 being R_eal st b1 <' b2 holds
ex b3 being R_eal st
( b1 <' b3 & b3 <' b2 & b3 in REAL )
proof end;

theorem Th18: :: MEASURE5:18
for b1, b2, b3 being R_eal st b1 <' b2 & b1 <' b3 holds
ex b4 being R_eal st
( b1 <' b4 & b4 <' b2 & b4 <' b3 & b4 in REAL )
proof end;

theorem Th19: :: MEASURE5:19
for b1, b2, b3 being R_eal st b1 <' b3 & b2 <' b3 holds
ex b4 being R_eal st
( b1 <' b4 & b2 <' b4 & b4 <' b3 & b4 in REAL )
proof end;

theorem Th20: :: MEASURE5:20
for b1, b2, b3, b4 being R_eal st b1 <' b2 & ( b1 <' b3 or b2 <' b4 ) holds
ex b5 being R_eal st
( ( b5 in ].b1,b3.[ & not b5 in ].b2,b4.[ ) or ( not b5 in ].b1,b3.[ & b5 in ].b2,b4.[ ) )
proof end;

theorem Th21: :: MEASURE5:21
for b1, b2, b3, b4 being R_eal st b1 <' b2 & ( b3 <' b1 or b4 <' b2 ) holds
ex b5 being R_eal st
( ( b5 in ].b3,b1.[ & not b5 in ].b4,b2.[ ) or ( not b5 in ].b3,b1.[ & b5 in ].b4,b2.[ ) )
proof end;

theorem Th22: :: MEASURE5:22
for b1, b2, b3, b4 being R_eal st b1 <' b2 & ( b1 <' b3 or b2 <' b4 ) holds
ex b5 being R_eal st
( ( b5 in [.b1,b3.] & not b5 in ].b2,b4.[ ) or ( not b5 in [.b1,b3.] & b5 in ].b2,b4.[ ) )
proof end;

theorem Th23: :: MEASURE5:23
for b1, b2, b3, b4 being R_eal st b1 <' b2 & ( b3 <' b1 or b4 <' b2 ) holds
ex b5 being R_eal st
( ( b5 in [.b3,b1.] & not b5 in ].b4,b2.[ ) or ( not b5 in [.b3,b1.] & b5 in ].b4,b2.[ ) )
proof end;

theorem Th24: :: MEASURE5:24
for b1, b2, b3, b4 being R_eal st b1 <' b2 & ( b1 <' b3 or b2 <' b4 ) holds
ex b5 being R_eal st
( ( b5 in ].b1,b3.[ & not b5 in [.b2,b4.] ) or ( not b5 in ].b1,b3.[ & b5 in [.b2,b4.] ) )
proof end;

theorem Th25: :: MEASURE5:25
for b1, b2, b3, b4 being R_eal st b1 <' b2 & ( b3 <' b1 or b4 <' b2 ) holds
ex b5 being R_eal st
( ( b5 in ].b3,b1.[ & not b5 in [.b4,b2.] ) or ( not b5 in ].b3,b1.[ & b5 in [.b4,b2.] ) )
proof end;

theorem Th26: :: MEASURE5:26
for b1, b2, b3, b4 being R_eal st b1 <' b2 & ( b1 <' b3 or b2 <' b4 ) holds
ex b5 being R_eal st
( ( b5 in ].b1,b3.[ & not b5 in [.b2,b4.[ ) or ( not b5 in ].b1,b3.[ & b5 in [.b2,b4.[ ) )
proof end;

theorem Th27: :: MEASURE5:27
for b1, b2, b3, b4 being R_eal st b1 <' b2 & ( b3 <' b1 or b4 <' b2 ) holds
ex b5 being R_eal st
( ( b5 in ].b3,b1.[ & not b5 in [.b4,b2.[ ) or ( not b5 in ].b3,b1.[ & b5 in [.b4,b2.[ ) )
proof end;

theorem Th28: :: MEASURE5:28
for b1, b2, b3, b4 being R_eal st b1 <' b2 & ( b1 <' b3 or b2 <' b4 ) holds
ex b5 being R_eal st
( ( b5 in [.b1,b3.[ & not b5 in ].b2,b4.[ ) or ( not b5 in [.b1,b3.[ & b5 in ].b2,b4.[ ) )
proof end;

theorem Th29: :: MEASURE5:29
for b1, b2, b3, b4 being R_eal st b1 <' b2 & ( b3 <' b1 or b4 <' b2 ) holds
ex b5 being R_eal st
( ( b5 in [.b3,b1.[ & not b5 in ].b4,b2.[ ) or ( not b5 in [.b3,b1.[ & b5 in ].b4,b2.[ ) )
proof end;

theorem Th30: :: MEASURE5:30
for b1, b2, b3, b4 being R_eal st b1 <' b2 & ( b1 <' b3 or b2 <' b4 ) holds
ex b5 being R_eal st
( ( b5 in ].b1,b3.[ & not b5 in ].b2,b4.] ) or ( not b5 in ].b1,b3.[ & b5 in ].b2,b4.] ) )
proof end;

theorem Th31: :: MEASURE5:31
for b1, b2, b3, b4 being R_eal st b1 <' b2 & ( b3 <' b1 or b4 <' b2 ) holds
ex b5 being R_eal st
( ( b5 in ].b3,b1.[ & not b5 in ].b4,b2.] ) or ( not b5 in ].b3,b1.[ & b5 in ].b4,b2.] ) )
proof end;

theorem Th32: :: MEASURE5:32
for b1, b2, b3, b4 being R_eal st b1 <' b2 & ( b1 <' b3 or b2 <' b4 ) holds
ex b5 being R_eal st
( ( b5 in ].b1,b3.] & not b5 in ].b2,b4.[ ) or ( not b5 in ].b1,b3.] & b5 in ].b2,b4.[ ) )
proof end;

theorem Th33: :: MEASURE5:33
for b1, b2, b3, b4 being R_eal st b1 <' b2 & ( b3 <' b1 or b4 <' b2 ) holds
ex b5 being R_eal st
( ( b5 in ].b3,b1.] & not b5 in ].b4,b2.[ ) or ( not b5 in ].b3,b1.] & b5 in ].b4,b2.[ ) )
proof end;

theorem Th34: :: MEASURE5:34
for b1, b2, b3, b4 being R_eal st b1 <' b2 & ( b1 <' b3 or b2 <' b4 ) holds
ex b5 being R_eal st
( ( b5 in [.b1,b3.] & not b5 in [.b2,b4.] ) or ( not b5 in [.b1,b3.] & b5 in [.b2,b4.] ) )
proof end;

theorem Th35: :: MEASURE5:35
for b1, b2, b3, b4 being R_eal st b1 <' b2 & ( b3 <' b1 or b4 <' b2 ) holds
ex b5 being R_eal st
( ( b5 in [.b3,b1.] & not b5 in [.b4,b2.] ) or ( not b5 in [.b3,b1.] & b5 in [.b4,b2.] ) )
proof end;

theorem Th36: :: MEASURE5:36
for b1, b2, b3, b4 being R_eal st b1 <' b2 & ( b1 <' b3 or b2 <' b4 ) holds
ex b5 being R_eal st
( ( b5 in [.b1,b3.] & not b5 in [.b2,b4.[ ) or ( not b5 in [.b1,b3.] & b5 in [.b2,b4.[ ) )
proof end;

theorem Th37: :: MEASURE5:37
for b1, b2, b3, b4 being R_eal st b1 <' b2 & ( b3 <' b1 or b4 <' b2 ) holds
ex b5 being R_eal st
( ( b5 in [.b3,b1.] & not b5 in [.b4,b2.[ ) or ( not b5 in [.b3,b1.] & b5 in [.b4,b2.[ ) )
proof end;

theorem Th38: :: MEASURE5:38
for b1, b2, b3, b4 being R_eal st b1 <' b2 & ( b1 <' b3 or b2 <' b4 ) holds
ex b5 being R_eal st
( ( b5 in [.b1,b3.[ & not b5 in [.b2,b4.] ) or ( not b5 in [.b1,b3.[ & b5 in [.b2,b4.] ) )
proof end;

theorem Th39: :: MEASURE5:39
for b1, b2, b3, b4 being R_eal st b1 <' b2 & ( b3 <' b1 or b4 <' b2 ) holds
ex b5 being R_eal st
( ( b5 in [.b3,b1.[ & not b5 in [.b4,b2.] ) or ( not b5 in [.b3,b1.[ & b5 in [.b4,b2.] ) )
proof end;

theorem Th40: :: MEASURE5:40
for b1, b2, b3, b4 being R_eal st b1 <' b2 & ( b1 <' b3 or b2 <' b4 ) holds
ex b5 being R_eal st
( ( b5 in [.b1,b3.] & not b5 in ].b2,b4.] ) or ( not b5 in [.b1,b3.] & b5 in ].b2,b4.] ) )
proof end;

theorem Th41: :: MEASURE5:41
for b1, b2, b3, b4 being R_eal st b1 <' b2 & ( b3 <' b1 or b4 <' b2 ) holds
ex b5 being R_eal st
( ( b5 in [.b3,b1.] & not b5 in ].b4,b2.] ) or ( not b5 in [.b3,b1.] & b5 in ].b4,b2.] ) )
proof end;

theorem Th42: :: MEASURE5:42
for b1, b2, b3, b4 being R_eal st b1 <' b2 & ( b1 <' b3 or b2 <' b4 ) holds
ex b5 being R_eal st
( ( b5 in ].b1,b3.] & not b5 in [.b2,b4.] ) or ( not b5 in ].b1,b3.] & b5 in [.b2,b4.] ) )
proof end;

theorem Th43: :: MEASURE5:43
for b1, b2, b3, b4 being R_eal st b1 <' b2 & ( b3 <' b1 or b4 <' b2 ) holds
ex b5 being R_eal st
( ( b5 in ].b3,b1.] & not b5 in [.b4,b2.] ) or ( not b5 in ].b3,b1.] & b5 in [.b4,b2.] ) )
proof end;

theorem Th44: :: MEASURE5:44
for b1, b2, b3, b4 being R_eal st b1 <' b2 & ( b1 <' b3 or b2 <' b4 ) holds
ex b5 being R_eal st
( ( b5 in [.b1,b3.[ & not b5 in [.b2,b4.[ ) or ( not b5 in [.b1,b3.[ & b5 in [.b2,b4.[ ) )
proof end;

theorem Th45: :: MEASURE5:45
for b1, b2, b3, b4 being R_eal st b1 <' b2 & ( b3 <' b1 or b4 <' b2 ) holds
ex b5 being R_eal st
( ( b5 in [.b3,b1.[ & not b5 in [.b4,b2.[ ) or ( not b5 in [.b3,b1.[ & b5 in [.b4,b2.[ ) )
proof end;

theorem Th46: :: MEASURE5:46
for b1, b2, b3, b4 being R_eal st b1 <' b2 & ( b1 <' b3 or b2 <' b4 ) holds
ex b5 being R_eal st
( ( b5 in [.b1,b3.[ & not b5 in ].b2,b4.] ) or ( not b5 in [.b1,b3.[ & b5 in ].b2,b4.] ) )
proof end;

theorem Th47: :: MEASURE5:47
for b1, b2, b3, b4 being R_eal st b1 <' b2 & ( b3 <' b1 or b4 <' b2 ) holds
ex b5 being R_eal st
( ( b5 in [.b3,b1.[ & not b5 in ].b4,b2.] ) or ( not b5 in [.b3,b1.[ & b5 in ].b4,b2.] ) )
proof end;

theorem Th48: :: MEASURE5:48
for b1, b2, b3, b4 being R_eal st b1 <' b2 & ( b1 <' b3 or b2 <' b4 ) holds
ex b5 being R_eal st
( ( b5 in ].b1,b3.] & not b5 in [.b2,b4.[ ) or ( not b5 in ].b1,b3.] & b5 in [.b2,b4.[ ) )
proof end;

theorem Th49: :: MEASURE5:49
for b1, b2, b3, b4 being R_eal st b1 <' b2 & ( b3 <' b1 or b4 <' b2 ) holds
ex b5 being R_eal st
( ( b5 in ].b3,b1.] & not b5 in [.b4,b2.[ ) or ( not b5 in ].b3,b1.] & b5 in [.b4,b2.[ ) )
proof end;

theorem Th50: :: MEASURE5:50
for b1, b2, b3, b4 being R_eal st b1 <' b2 & ( b1 <' b3 or b2 <' b4 ) holds
ex b5 being R_eal st
( ( b5 in ].b1,b3.] & not b5 in ].b2,b4.] ) or ( not b5 in ].b1,b3.] & b5 in ].b2,b4.] ) )
proof end;

theorem Th51: :: MEASURE5:51
for b1, b2, b3, b4 being R_eal st b1 <' b2 & ( b3 <' b1 or b4 <' b2 ) holds
ex b5 being R_eal st
( ( b5 in ].b3,b1.] & not b5 in ].b4,b2.] ) or ( not b5 in ].b3,b1.] & b5 in ].b4,b2.] ) )
proof end;

theorem Th52: :: MEASURE5:52
for b1, b2, b3, b4 being R_eal
for b5 being Interval st b1 <' b2 & ( b5 = ].b1,b2.[ or b5 = [.b1,b2.] or b5 = [.b1,b2.[ or b5 = ].b1,b2.] ) & ( b5 = ].b3,b4.[ or b5 = [.b3,b4.] or b5 = [.b3,b4.[ or b5 = ].b3,b4.] ) holds
( b1 = b3 & b2 = b4 )
proof end;

definition
let c1 be Interval;
func vol c1 -> R_eal means :Def10: :: MEASURE5:def 10
ex b1, b2 being R_eal st
( ( a1 = ].b1,b2.[ or a1 = [.b1,b2.] or a1 = [.b1,b2.[ or a1 = ].b1,b2.] ) & ( b1 <' b2 implies a2 = b2 - b1 ) & ( b2 <=' b1 implies a2 = 0. ) );
existence
ex b1, b2, b3 being R_eal st
( ( c1 = ].b2,b3.[ or c1 = [.b2,b3.] or c1 = [.b2,b3.[ or c1 = ].b2,b3.] ) & ( b2 <' b3 implies b1 = b3 - b2 ) & ( b3 <=' b2 implies b1 = 0. ) )
proof end;
uniqueness
for b1, b2 being R_eal st ex b3, b4 being R_eal st
( ( c1 = ].b3,b4.[ or c1 = [.b3,b4.] or c1 = [.b3,b4.[ or c1 = ].b3,b4.] ) & ( b3 <' b4 implies b1 = b4 - b3 ) & ( b4 <=' b3 implies b1 = 0. ) ) & ex b3, b4 being R_eal st
( ( c1 = ].b3,b4.[ or c1 = [.b3,b4.] or c1 = [.b3,b4.[ or c1 = ].b3,b4.] ) & ( b3 <' b4 implies b2 = b4 - b3 ) & ( b4 <=' b3 implies b2 = 0. ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines vol MEASURE5:def 10 :
for b1 being Interval
for b2 being R_eal holds
( b2 = vol b1 iff ex b3, b4 being R_eal st
( ( b1 = ].b3,b4.[ or b1 = [.b3,b4.] or b1 = [.b3,b4.[ or b1 = ].b3,b4.] ) & ( b3 <' b4 implies b2 = b4 - b3 ) & ( b4 <=' b3 implies b2 = 0. ) ) );

theorem Th53: :: MEASURE5:53
for b1 being open_interval Subset of REAL
for b2, b3 being R_eal st b1 = ].b2,b3.[ holds
( ( b2 <' b3 implies vol b1 = b3 - b2 ) & ( b3 <=' b2 implies vol b1 = 0. ) ) by Def10;

theorem Th54: :: MEASURE5:54
for b1 being closed_interval Subset of REAL
for b2, b3 being R_eal st b1 = [.b2,b3.] holds
( ( b2 <' b3 implies vol b1 = b3 - b2 ) & ( b3 <=' b2 implies vol b1 = 0. ) ) by Def10;

theorem Th55: :: MEASURE5:55
for b1 being right_open_interval Subset of REAL
for b2, b3 being R_eal st b1 = [.b2,b3.[ holds
( ( b2 <' b3 implies vol b1 = b3 - b2 ) & ( b3 <=' b2 implies vol b1 = 0. ) ) by Def10;

theorem Th56: :: MEASURE5:56
for b1 being left_open_interval Subset of REAL
for b2, b3 being R_eal st b1 = ].b2,b3.] holds
( ( b2 <' b3 implies vol b1 = b3 - b2 ) & ( b3 <=' b2 implies vol b1 = 0. ) ) by Def10;

theorem Th57: :: MEASURE5:57
for b1 being Interval
for b2, b3, b4 being R_eal st b2 = -infty & b3 in REAL & b4 = +infty & ( b1 = ].b2,b3.[ or b1 = ].b3,b4.[ or b1 = [.b2,b3.] or b1 = [.b3,b4.] or b1 = [.b2,b3.[ or b1 = [.b3,b4.[ or b1 = ].b2,b3.] or b1 = ].b3,b4.] ) holds
vol b1 = +infty
proof end;

theorem Th58: :: MEASURE5:58
for b1 being Interval
for b2, b3 being R_eal st b2 = -infty & b3 = +infty & ( b1 = ].b2,b3.[ or b1 = [.b2,b3.] or b1 = [.b2,b3.[ or b1 = ].b2,b3.] ) holds
vol b1 = +infty
proof end;

registration
cluster empty Element of K40(REAL );
existence
ex b1 being Interval st b1 is empty
proof end;
end;

definition
redefine func {} as {} -> empty Interval;
coherence
{} is empty Interval
proof end;
end;

theorem Th59: :: MEASURE5:59
canceled;

theorem Th60: :: MEASURE5:60
vol {} = 0.
proof end;

theorem Th61: :: MEASURE5:61
for b1, b2 being R_eal
for b3, b4 being Interval st b3 c= b4 & b4 = [.b1,b2.] & b2 <=' b1 holds
( vol b3 = 0. & vol b4 = 0. )
proof end;

theorem Th62: :: MEASURE5:62
for b1, b2 being Interval st b1 c= b2 holds
vol b1 <=' vol b2
proof end;

theorem Th63: :: MEASURE5:63
for b1 being Interval holds 0. <=' vol b1
proof end;