Z1: now :: thesis: ( Dcb . 1 <> upper_bound Iac implies Dac ^ Dcb is non empty increasing FinSequence of REAL )
assume A2: Dcb . 1 <> upper_bound Iac ; :: thesis: Dac ^ Dcb is non empty increasing FinSequence of REAL
A3: Dac . (len Dac) = upper_bound Iac by INTEGRA1:def 2;
A4: Dac . (len Dac) <= lower_bound Icb by A1, INTEGRA1:def 2;
A5: rng Dcb c= Icb by INTEGRA1:def 2;
rng Dcb <> {} ;
then 1 in dom Dcb by FINSEQ_3:32;
then A6: Dcb . 1 in Icb by A5, FUNCT_1:3;
consider c, b being Real such that
A7: Icb = [.c,b.] by MEASURE5:def 3;
c <= b by A7, XXREAL_1:29;
then lower_bound Icb = c by A7, JORDAN5A:19;
then lower_bound Icb <= Dcb . 1 by A6, A7, XXREAL_1:1;
then Dac . (len Dac) <= Dcb . 1 by A4, XXREAL_0:2;
then Dac . (len Dac) < Dcb . 1 by A3, A2, XXREAL_0:1;
hence Dac ^ Dcb is non empty increasing FinSequence of REAL by Th1; :: thesis: verum
end;
now :: thesis: ( Dcb . 1 = upper_bound Iac implies Dac ^ (Dcb /^ 1) is non empty increasing FinSequence of REAL )
assume A8: Dcb . 1 = upper_bound Iac ; :: thesis: Dac ^ (Dcb /^ 1) is non empty increasing FinSequence of REAL
now :: thesis: ( not Dcb /^ 1 is empty implies Dac ^ (Dcb /^ 1) is non empty increasing FinSequence of REAL )
assume A9: not Dcb /^ 1 is empty ; :: thesis: Dac ^ (Dcb /^ 1) is non empty increasing FinSequence of REAL
then A10: rng (Dcb /^ 1) <> {} ;
rng Dcb <> {} ;
then A11: 1 in dom Dcb by FINSEQ_3:32;
then A12: 1 <= len Dcb by FINSEQ_3:25;
then reconsider D2 = Dcb /^ 1 as non empty increasing FinSequence of REAL by A9, INTEGRA1:34;
A13: Dac . (len Dac) = upper_bound Iac by INTEGRA1:def 2;
1 in dom (Dcb /^ 1) by A10, FINSEQ_3:32;
then A14: (Dcb /^ 1) . 1 = Dcb . (1 + 1) by A12, RFINSEQ:def 1;
1 in dom (Dcb /^ 1) by A10, FINSEQ_3:32;
then 1 + 1 in dom Dcb by FINSEQ_5:26;
then upper_bound Iac < D2 . 1 by A8, A14, A11, VALUED_0:def 13;
hence Dac ^ (Dcb /^ 1) is non empty increasing FinSequence of REAL by A13, Th1; :: thesis: verum
end;
hence Dac ^ (Dcb /^ 1) is non empty increasing FinSequence of REAL by FINSEQ_1:34; :: thesis: verum
end;
hence ( ( Dcb . 1 <> upper_bound Iac implies Dac ^ Dcb is non empty increasing FinSequence of REAL ) & ( not Dcb . 1 <> upper_bound Iac implies Dac ^ (Dcb /^ 1) is non empty increasing FinSequence of REAL ) & ( for b1 being non empty increasing FinSequence of REAL holds verum ) ) by Z1; :: thesis: verum