let A be non empty closed_interval Subset of REAL; :: thesis: for D being Division of A
for t being Element of A st lower_bound A < D . 1 holds
ex i being Element of NAT st
( i in dom D & t in divset (D,i) & ( i = 1 or ( lower_bound (divset (D,i)) < t & t <= upper_bound (divset (D,i)) ) ) )
let D be Division of A; :: thesis: for t being Element of A st lower_bound A < D . 1 holds
ex i being Element of NAT st
( i in dom D & t in divset (D,i) & ( i = 1 or ( lower_bound (divset (D,i)) < t & t <= upper_bound (divset (D,i)) ) ) )
let t be Element of A; :: thesis: ( lower_bound A < D . 1 implies ex i being Element of NAT st
( i in dom D & t in divset (D,i) & ( i = 1 or ( lower_bound (divset (D,i)) < t & t <= upper_bound (divset (D,i)) ) ) ) )
assume AS: lower_bound A < D . 1 ; :: thesis: ex i being Element of NAT st
( i in dom D & t in divset (D,i) & ( i = 1 or ( lower_bound (divset (D,i)) < t & t <= upper_bound (divset (D,i)) ) ) )
consider i being Element of NAT such that
A24: i in dom D and
A25: t in divset (D,i) by INTEGRA3:3;

per cases ( i = 1 or i <> 1 ) ;

suppose i = 1 ; :: thesis: ex i being Element of NAT st
( i in dom D & t in divset (D,i) & ( i = 1 or ( lower_bound (divset (D,i)) < t & t <= upper_bound (divset (D,i)) ) ) )

hence ex i being Element of NAT st
( i in dom D & t in divset (D,i) & ( i = 1 or ( lower_bound (divset (D,i)) < t & t <= upper_bound (divset (D,i)) ) ) ) by A24, A25; :: thesis: verum

end;

suppose A26: i <> 1 ; :: thesis: ex i being Element of NAT st
( i in dom D & t in divset (D,i) & ( i = 1 or ( lower_bound (divset (D,i)) < t & t <= upper_bound (divset (D,i)) ) ) )

t in [.(lower_bound (divset (D,i))),(upper_bound (divset (D,i))).] by A25, INTEGRA1:4;
then A30: ( lower_bound (divset (D,i)) <= t & t <= upper_bound (divset (D,i)) ) by XXREAL_1:1;
thus ex i being Element of NAT st
( i in dom D & t in divset (D,i) & ( i = 1 or ( lower_bound (divset (D,i)) < t & t <= upper_bound (divset (D,i)) ) ) ) :: thesis: verum

proof

per cases ( not lower_bound (divset (D,i)) = t or lower_bound (divset (D,i)) = t ) ;

suppose not lower_bound (divset (D,i)) = t ; :: thesis: ex i being Element of NAT st
( i in dom D & t in divset (D,i) & ( i = 1 or ( lower_bound (divset (D,i)) < t & t <= upper_bound (divset (D,i)) ) ) )

then lower_bound (divset (D,i)) < t by A30, XXREAL_0:1;
hence ex i being Element of NAT st
( i in dom D & t in divset (D,i) & ( i = 1 or ( lower_bound (divset (D,i)) < t & t <= upper_bound (divset (D,i)) ) ) ) by A24, A25, A30; :: thesis: verum

end;

suppose A31: lower_bound (divset (D,i)) = t ; :: thesis: ex i being Element of NAT st
( i in dom D & t in divset (D,i) & ( i = 1 or ( lower_bound (divset (D,i)) < t & t <= upper_bound (divset (D,i)) ) ) )

A38: i - 1 in dom D by A24, A26, INTEGRA1:7;
reconsider j = i - 1 as Element of NAT by A24, A26, INTEGRA1:7;
A40: ( t = upper_bound (divset (D,j)) & t in divset (D,j) )

proof

( j = 1 or j <> 1 ) ;
then upper_bound (divset (D,j)) = D . (i - 1) by A38, INTEGRA1:def 4;
hence A41: t = upper_bound (divset (D,j)) by A31, A24, A26, INTEGRA1:def 4; :: thesis: t in divset (D,j)
lower_bound (divset (D,j)) <= upper_bound (divset (D,j)) by SEQ_4:11;
then t in [.(lower_bound (divset (D,j))),(upper_bound (divset (D,j))).] by A41;
hence t in divset (D,j) by INTEGRA1:4; :: thesis: verum

end;

lower_bound (divset (D,j)) < upper_bound (divset (D,j))

proof

per cases ( j = 1 or j <> 1 ) ;

suppose A42: j = 1 ; :: thesis: lower_bound (divset (D,j)) < upper_bound (divset (D,j))

then ( lower_bound (divset (D,j)) = lower_bound A & upper_bound (divset (D,j)) = D . j ) by A38, INTEGRA1:def 4;
hence lower_bound (divset (D,j)) < upper_bound (divset (D,j)) by AS, A42; :: thesis: verum

end;

suppose A44: j <> 1 ; :: thesis: lower_bound (divset (D,j)) < upper_bound (divset (D,j))

then A45: ( lower_bound (divset (D,j)) = D . (j - 1) & upper_bound (divset (D,j)) = D . j ) by A38, INTEGRA1:def 4;
j - 1 in dom D by A38, A44, INTEGRA1:7;
hence lower_bound (divset (D,j)) < upper_bound (divset (D,j)) by A45, A38, XREAL_1:146, VALUED_0:def 13; :: thesis: verum

end;

end;

end;

hence ex i being Element of NAT st
( i in dom D & t in divset (D,i) & ( i = 1 or ( lower_bound (divset (D,i)) < t & t <= upper_bound (divset (D,i)) ) ) ) by A38, A40; :: thesis: verum

end;

end;

end;

end;

end;