let i be Element of NAT ; :: thesis: for A being non empty closed_interval Subset of REAL
for D being Division of A st i in dom D holds
ex A1, A2 being non empty closed_interval Subset of REAL st
( A1 = [.(lower_bound A),(D . i).] & A2 = [.(D . i),(upper_bound A).] & A = A1 \/ A2 )
let A be non empty closed_interval Subset of REAL; :: thesis: for D being Division of A st i in dom D holds
ex A1, A2 being non empty closed_interval Subset of REAL st
( A1 = [.(lower_bound A),(D . i).] & A2 = [.(D . i),(upper_bound A).] & A = A1 \/ A2 )
let D be Division of A; :: thesis: ( i in dom D implies ex A1, A2 being non empty closed_interval Subset of REAL st
( A1 = [.(lower_bound A),(D . i).] & A2 = [.(D . i),(upper_bound A).] & A = A1 \/ A2 ) )
assume i in dom D ; :: thesis: ex A1, A2 being non empty closed_interval Subset of REAL st
( A1 = [.(lower_bound A),(D . i).] & A2 = [.(D . i),(upper_bound A).] & A = A1 \/ A2 )
then A1: D . i in rng D by FUNCT_1:def 3;
rng D c= A by Def1;
then D . i in A by A1;
then D . i in [.(lower_bound A),(upper_bound A).] by Th2;
then D . i in { a where a is Real : ( lower_bound A <= a & a <= upper_bound A ) } by RCOMP_1:def 1;
then A2: ex a being Real st
( a = D . i & lower_bound A <= a & a <= upper_bound A ) ;
then reconsider A1 = [.(lower_bound A),(D . i).] as non empty closed_interval Subset of REAL by MEASURE5:14;
reconsider A2 = [.(D . i),(upper_bound A).] as non empty closed_interval Subset of REAL by A2, MEASURE5:14;
take A1 ; :: thesis: ex A2 being non empty closed_interval Subset of REAL st
( A1 = [.(lower_bound A),(D . i).] & A2 = [.(D . i),(upper_bound A).] & A = A1 \/ A2 )
take A2 ; :: thesis: ( A1 = [.(lower_bound A),(D . i).] & A2 = [.(D . i),(upper_bound A).] & A = A1 \/ A2 )
A1 \/ A2 = [.(lower_bound A),(upper_bound A).] by A2, XXREAL_1:174
.= A by Th2 ;
hence ( A1 = [.(lower_bound A),(D . i).] & A2 = [.(D . i),(upper_bound A).] & A = A1 \/ A2 ) ; :: thesis: verum