let i be Element of NAT ; :: thesis: for A being closed-interval Subset of REAL
for D being Division of A st i in dom D holds
ex A1, A2 being closed-interval Subset of REAL st
( A1 = [.(lower_bound A),(D . i).] & A2 = [.(D . i),(upper_bound A).] & A = A1 \/ A2 )
let A be closed-interval Subset of REAL ; :: thesis: for D being Division of A st i in dom D holds
ex A1, A2 being 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 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 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 5;
rng D c= A by Def2;
then D . i in A by A1;
then D . i in [.(lower_bound A),(upper_bound A).] by Th5;
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 closed-interval Subset of REAL by Def1;
reconsider A2 = [.(D . i),(upper_bound A).] as closed-interval Subset of REAL by A2, Def1;
take A1 ; :: thesis: ex A2 being 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 Th5 ;
hence ( A1 = [.(lower_bound A),(D . i).] & A2 = [.(D . i),(upper_bound A).] & A = A1 \/ A2 ) ; :: thesis: verum