:: MEASURE5 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: MEASURE5:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being R_eal st x <> -infty & x <> +infty & x <=' y holds
0. <=' y - x
proof end;

theorem Th2: :: MEASURE5:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being R_eal st ( not x = -infty or not y = -infty ) & ( not x = +infty or not y = +infty ) & x <=' y holds
0. <=' y - x
proof end;

theorem :: MEASURE5:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: MEASURE5:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: MEASURE5:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: MEASURE5:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: MEASURE5:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: MEASURE5:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being R_eal st b <> -infty & b <> +infty & ( not a = -infty or not c = -infty ) & ( not a = +infty or not c = +infty ) holds
(c - b) + (b - a) = c - a
proof end;

theorem :: MEASURE5:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a1, a2 being R_eal holds
( inf {a1,a2} <=' a1 & inf {a1,a2} <=' a2 & a1 <=' sup {a1,a2} & a2 <=' sup {a1,a2} )
proof end;

scheme :: MEASURE5:sch 1
RSetEq{ P1[ set ] } :
for X1, X2 being Subset of REAL st ( for x being R_eal holds
( x in X1 iff P1[x] ) ) & ( for x being R_eal holds
( x in X2 iff P1[x] ) ) holds
X1 = X2
proof end;

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

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

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

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

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

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

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

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

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 IT be Subset of REAL ;
attr IT is right_open_interval means :Def7: :: MEASURE5:def 7
 ex a, b being R_eal st
( a <=' b & IT = [.a,b.[ );
end;

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

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

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

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

notation
let IT be Subset of REAL ;
synonym right_closed_interval IT for left_open_interval IT;
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 IT be Subset of REAL ;
attr IT is interval means :Def9: :: MEASURE5:def 9
( IT is open_interval or IT is closed_interval or IT is right_open_interval or IT is left_open_interval );
end;

:: deftheorem Def9 defines interval MEASURE5:def 9 :
for IT being Subset of REAL holds
( IT is interval iff ( IT is open_interval or IT is closed_interval or IT is right_open_interval or IT 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 :: MEASURE5:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th11: :: MEASURE5:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for a, b being R_eal st ( x in ].a,b.[ or x in [.a,b.] or x in [.a,b.[ or x in ].a,b.] ) holds
x is R_eal
proof end;

theorem Th12: :: MEASURE5:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being R_eal st b <' a holds
( ].a,b.[ = {} & [.a,b.] = {} & [.a,b.[ = {} & ].a,b.] = {} )
proof end;

theorem Th13: :: MEASURE5:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being R_eal holds
( ].a,a.[ = {} & [.a,a.[ = {} & ].a,a.] = {} )
proof end;

theorem Th14: :: MEASURE5:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being R_eal holds
( ( ( a = -infty or a = +infty ) implies [.a,a.] = {} ) & ( a <> -infty & a <> +infty implies [.a,a.] = {a} ) )
proof end;

theorem Th15: :: MEASURE5:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being R_eal st b <=' a holds
( ].a,b.[ = {} & [.a,b.[ = {} & ].a,b.] = {} & [.a,b.] c= {a} & [.a,b.] c= {b} )
proof end;

theorem :: MEASURE5:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being R_eal st a <' b & b <' c holds
b in REAL
proof end;

theorem Th17: :: MEASURE5:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being R_eal st a <' b holds
ex x being R_eal st
( a <' x & x <' b & x in REAL )
proof end;

theorem Th18: :: MEASURE5:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being R_eal st a <' b & a <' c holds
ex x being R_eal st
( a <' x & x <' b & x <' c & x in REAL )
proof end;

theorem Th19: :: MEASURE5:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being R_eal st a <' c & b <' c holds
ex x being R_eal st
( a <' x & b <' x & x <' c & x in REAL )
proof end;

theorem Th20: :: MEASURE5:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a1, a2, b1, b2 being R_eal st a1 <' a2 & ( a1 <' b1 or a2 <' b2 ) holds
ex x being R_eal st
( ( x in ].a1,b1.[ & not x in ].a2,b2.[ ) or ( not x in ].a1,b1.[ & x in ].a2,b2.[ ) )
proof end;

theorem Th21: :: MEASURE5:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for b1, b2, a1, a2 being R_eal st b1 <' b2 & ( a1 <' b1 or a2 <' b2 ) holds
ex x being R_eal st
( ( x in ].a1,b1.[ & not x in ].a2,b2.[ ) or ( not x in ].a1,b1.[ & x in ].a2,b2.[ ) )
proof end;

theorem Th22: :: MEASURE5:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a1, a2, b1, b2 being R_eal st a1 <' a2 & ( a1 <' b1 or a2 <' b2 ) holds
ex x being R_eal st
( ( x in [.a1,b1.] & not x in ].a2,b2.[ ) or ( not x in [.a1,b1.] & x in ].a2,b2.[ ) )
proof end;

theorem Th23: :: MEASURE5:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for b1, b2, a1, a2 being R_eal st b1 <' b2 & ( a1 <' b1 or a2 <' b2 ) holds
ex x being R_eal st
( ( x in [.a1,b1.] & not x in ].a2,b2.[ ) or ( not x in [.a1,b1.] & x in ].a2,b2.[ ) )
proof end;

theorem Th24: :: MEASURE5:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a1, a2, b1, b2 being R_eal st a1 <' a2 & ( a1 <' b1 or a2 <' b2 ) holds
ex x being R_eal st
( ( x in ].a1,b1.[ & not x in [.a2,b2.] ) or ( not x in ].a1,b1.[ & x in [.a2,b2.] ) )
proof end;

theorem Th25: :: MEASURE5:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for b1, b2, a1, a2 being R_eal st b1 <' b2 & ( a1 <' b1 or a2 <' b2 ) holds
ex x being R_eal st
( ( x in ].a1,b1.[ & not x in [.a2,b2.] ) or ( not x in ].a1,b1.[ & x in [.a2,b2.] ) )
proof end;

theorem Th26: :: MEASURE5:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a1, a2, b1, b2 being R_eal st a1 <' a2 & ( a1 <' b1 or a2 <' b2 ) holds
ex x being R_eal st
( ( x in ].a1,b1.[ & not x in [.a2,b2.[ ) or ( not x in ].a1,b1.[ & x in [.a2,b2.[ ) )
proof end;

theorem Th27: :: MEASURE5:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for b1, b2, a1, a2 being R_eal st b1 <' b2 & ( a1 <' b1 or a2 <' b2 ) holds
ex x being R_eal st
( ( x in ].a1,b1.[ & not x in [.a2,b2.[ ) or ( not x in ].a1,b1.[ & x in [.a2,b2.[ ) )
proof end;

theorem Th28: :: MEASURE5:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a1, a2, b1, b2 being R_eal st a1 <' a2 & ( a1 <' b1 or a2 <' b2 ) holds
ex x being R_eal st
( ( x in [.a1,b1.[ & not x in ].a2,b2.[ ) or ( not x in [.a1,b1.[ & x in ].a2,b2.[ ) )
proof end;

theorem Th29: :: MEASURE5:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for b1, b2, a1, a2 being R_eal st b1 <' b2 & ( a1 <' b1 or a2 <' b2 ) holds
ex x being R_eal st
( ( x in [.a1,b1.[ & not x in ].a2,b2.[ ) or ( not x in [.a1,b1.[ & x in ].a2,b2.[ ) )
proof end;

theorem Th30: :: MEASURE5:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a1, a2, b1, b2 being R_eal st a1 <' a2 & ( a1 <' b1 or a2 <' b2 ) holds
ex x being R_eal st
( ( x in ].a1,b1.[ & not x in ].a2,b2.] ) or ( not x in ].a1,b1.[ & x in ].a2,b2.] ) )
proof end;

theorem Th31: :: MEASURE5:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for b1, b2, a1, a2 being R_eal st b1 <' b2 & ( a1 <' b1 or a2 <' b2 ) holds
ex x being R_eal st
( ( x in ].a1,b1.[ & not x in ].a2,b2.] ) or ( not x in ].a1,b1.[ & x in ].a2,b2.] ) )
proof end;

theorem Th32: :: MEASURE5:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a1, a2, b1, b2 being R_eal st a1 <' a2 & ( a1 <' b1 or a2 <' b2 ) holds
ex x being R_eal st
( ( x in ].a1,b1.] & not x in ].a2,b2.[ ) or ( not x in ].a1,b1.] & x in ].a2,b2.[ ) )
proof end;

theorem Th33: :: MEASURE5:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for b1, b2, a1, a2 being R_eal st b1 <' b2 & ( a1 <' b1 or a2 <' b2 ) holds
ex x being R_eal st
( ( x in ].a1,b1.] & not x in ].a2,b2.[ ) or ( not x in ].a1,b1.] & x in ].a2,b2.[ ) )
proof end;

theorem Th34: :: MEASURE5:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a1, a2, b1, b2 being R_eal st a1 <' a2 & ( a1 <' b1 or a2 <' b2 ) holds
ex x being R_eal st
( ( x in [.a1,b1.] & not x in [.a2,b2.] ) or ( not x in [.a1,b1.] & x in [.a2,b2.] ) )
proof end;

theorem Th35: :: MEASURE5:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for b1, b2, a1, a2 being R_eal st b1 <' b2 & ( a1 <' b1 or a2 <' b2 ) holds
ex x being R_eal st
( ( x in [.a1,b1.] & not x in [.a2,b2.] ) or ( not x in [.a1,b1.] & x in [.a2,b2.] ) )
proof end;

theorem Th36: :: MEASURE5:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a1, a2, b1, b2 being R_eal st a1 <' a2 & ( a1 <' b1 or a2 <' b2 ) holds
ex x being R_eal st
( ( x in [.a1,b1.] & not x in [.a2,b2.[ ) or ( not x in [.a1,b1.] & x in [.a2,b2.[ ) )
proof end;

theorem Th37: :: MEASURE5:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for b1, b2, a1, a2 being R_eal st b1 <' b2 & ( a1 <' b1 or a2 <' b2 ) holds
ex x being R_eal st
( ( x in [.a1,b1.] & not x in [.a2,b2.[ ) or ( not x in [.a1,b1.] & x in [.a2,b2.[ ) )
proof end;

theorem Th38: :: MEASURE5:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a1, a2, b1, b2 being R_eal st a1 <' a2 & ( a1 <' b1 or a2 <' b2 ) holds
ex x being R_eal st
( ( x in [.a1,b1.[ & not x in [.a2,b2.] ) or ( not x in [.a1,b1.[ & x in [.a2,b2.] ) )
proof end;

theorem Th39: :: MEASURE5:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for b1, b2, a1, a2 being R_eal st b1 <' b2 & ( a1 <' b1 or a2 <' b2 ) holds
ex x being R_eal st
( ( x in [.a1,b1.[ & not x in [.a2,b2.] ) or ( not x in [.a1,b1.[ & x in [.a2,b2.] ) )
proof end;

theorem Th40: :: MEASURE5:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a1, a2, b1, b2 being R_eal st a1 <' a2 & ( a1 <' b1 or a2 <' b2 ) holds
ex x being R_eal st
( ( x in [.a1,b1.] & not x in ].a2,b2.] ) or ( not x in [.a1,b1.] & x in ].a2,b2.] ) )
proof end;

theorem Th41: :: MEASURE5:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for b1, b2, a1, a2 being R_eal st b1 <' b2 & ( a1 <' b1 or a2 <' b2 ) holds
ex x being R_eal st
( ( x in [.a1,b1.] & not x in ].a2,b2.] ) or ( not x in [.a1,b1.] & x in ].a2,b2.] ) )
proof end;

theorem Th42: :: MEASURE5:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a1, a2, b1, b2 being R_eal st a1 <' a2 & ( a1 <' b1 or a2 <' b2 ) holds
ex x being R_eal st
( ( x in ].a1,b1.] & not x in [.a2,b2.] ) or ( not x in ].a1,b1.] & x in [.a2,b2.] ) )
proof end;

theorem Th43: :: MEASURE5:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for b1, b2, a1, a2 being R_eal st b1 <' b2 & ( a1 <' b1 or a2 <' b2 ) holds
ex x being R_eal st
( ( x in ].a1,b1.] & not x in [.a2,b2.] ) or ( not x in ].a1,b1.] & x in [.a2,b2.] ) )
proof end;

theorem Th44: :: MEASURE5:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a1, a2, b1, b2 being R_eal st a1 <' a2 & ( a1 <' b1 or a2 <' b2 ) holds
ex x being R_eal st
( ( x in [.a1,b1.[ & not x in [.a2,b2.[ ) or ( not x in [.a1,b1.[ & x in [.a2,b2.[ ) )
proof end;

theorem Th45: :: MEASURE5:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for b1, b2, a1, a2 being R_eal st b1 <' b2 & ( a1 <' b1 or a2 <' b2 ) holds
ex x being R_eal st
( ( x in [.a1,b1.[ & not x in [.a2,b2.[ ) or ( not x in [.a1,b1.[ & x in [.a2,b2.[ ) )
proof end;

theorem Th46: :: MEASURE5:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a1, a2, b1, b2 being R_eal st a1 <' a2 & ( a1 <' b1 or a2 <' b2 ) holds
ex x being R_eal st
( ( x in [.a1,b1.[ & not x in ].a2,b2.] ) or ( not x in [.a1,b1.[ & x in ].a2,b2.] ) )
proof end;

theorem Th47: :: MEASURE5:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for b1, b2, a1, a2 being R_eal st b1 <' b2 & ( a1 <' b1 or a2 <' b2 ) holds
ex x being R_eal st
( ( x in [.a1,b1.[ & not x in ].a2,b2.] ) or ( not x in [.a1,b1.[ & x in ].a2,b2.] ) )
proof end;

theorem Th48: :: MEASURE5:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a1, a2, b1, b2 being R_eal st a1 <' a2 & ( a1 <' b1 or a2 <' b2 ) holds
ex x being R_eal st
( ( x in ].a1,b1.] & not x in [.a2,b2.[ ) or ( not x in ].a1,b1.] & x in [.a2,b2.[ ) )
proof end;

theorem Th49: :: MEASURE5:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for b1, b2, a1, a2 being R_eal st b1 <' b2 & ( a1 <' b1 or a2 <' b2 ) holds
ex x being R_eal st
( ( x in ].a1,b1.] & not x in [.a2,b2.[ ) or ( not x in ].a1,b1.] & x in [.a2,b2.[ ) )
proof end;

theorem Th50: :: MEASURE5:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a1, a2, b1, b2 being R_eal st a1 <' a2 & ( a1 <' b1 or a2 <' b2 ) holds
ex x being R_eal st
( ( x in ].a1,b1.] & not x in ].a2,b2.] ) or ( not x in ].a1,b1.] & x in ].a2,b2.] ) )
proof end;

theorem Th51: :: MEASURE5:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for b1, b2, a1, a2 being R_eal st b1 <' b2 & ( a1 <' b1 or a2 <' b2 ) holds
ex x being R_eal st
( ( x in ].a1,b1.] & not x in ].a2,b2.] ) or ( not x in ].a1,b1.] & x in ].a2,b2.] ) )
proof end;

theorem Th52: :: MEASURE5:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a1, b1, a2, b2 being R_eal
for A being Interval st a1 <' b1 & ( A = ].a1,b1.[ or A = [.a1,b1.] or A = [.a1,b1.[ or A = ].a1,b1.] ) & ( A = ].a2,b2.[ or A = [.a2,b2.] or A = [.a2,b2.[ or A = ].a2,b2.] ) holds
( a1 = a2 & b1 = b2 )
proof end;

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

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

theorem :: MEASURE5:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being open_interval Subset of REAL
for a, b being R_eal st A = ].a,b.[ holds
( ( a <' b implies vol A = b - a ) & ( b <=' a implies vol A = 0. ) ) by Def10;

theorem :: MEASURE5:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being closed_interval Subset of REAL
for a, b being R_eal st A = [.a,b.] holds
( ( a <' b implies vol A = b - a ) & ( b <=' a implies vol A = 0. ) ) by Def10;

theorem :: MEASURE5:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being right_open_interval Subset of REAL
for a, b being R_eal st A = [.a,b.[ holds
( ( a <' b implies vol A = b - a ) & ( b <=' a implies vol A = 0. ) ) by Def10;

theorem :: MEASURE5:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being left_open_interval Subset of REAL
for a, b being R_eal st A = ].a,b.] holds
( ( a <' b implies vol A = b - a ) & ( b <=' a implies vol A = 0. ) ) by Def10;

theorem :: MEASURE5:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Interval
for a, b, c being R_eal st a = -infty & b in REAL & c = +infty & ( A = ].a,b.[ or A = ].b,c.[ or A = [.a,b.] or A = [.b,c.] or A = [.a,b.[ or A = [.b,c.[ or A = ].a,b.] or A = ].b,c.] ) holds
vol A = +infty
proof end;

theorem :: MEASURE5:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Interval
for a, b being R_eal st a = -infty & b = +infty & ( A = ].a,b.[ or A = [.a,b.] or A = [.a,b.[ or A = ].a,b.] ) holds
vol A = +infty
proof end;

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

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

theorem :: MEASURE5:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th60: :: MEASURE5:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
vol {} = 0.
proof end;

theorem Th61: :: MEASURE5:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being R_eal
for A, B being Interval st A c= B & B = [.a,b.] & b <=' a holds
( vol A = 0. & vol B = 0. )
proof end;

theorem Th62: :: MEASURE5:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being Interval st A c= B holds
vol A <=' vol B
proof end;

theorem :: MEASURE5:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Interval holds 0. <=' vol A
proof end;