let a, b be Real; :: thesis: for Iab being non empty closed_interval Subset of REAL st a < b & Iab = [.a,b.] holds
<*a,b*> is Division of Iab
let Iab be non empty closed_interval Subset of REAL; :: thesis: ( a < b & Iab = [.a,b.] implies <*a,b*> is Division of Iab )
assume that
A1: a < b and
A2: Iab = [.a,b.] ; :: thesis: <*a,b*> is Division of Iab
set D = <*a,b*>;
A3: <*a,b*> is non empty increasing FinSequence of REAL by A1, Th45;
A4: rng <*a,b*> c= Iab
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng <*a,b*> or x in Iab )
assume x in rng <*a,b*> ; :: thesis: x in Iab
then x in {a,b} by FINSEQ_2:127;
then ( x = a or x = b ) by TARSKI:def 2;
hence x in Iab by A1, A2, XXREAL_1:1; :: thesis: verum
end;
<*a,b*> . (len <*a,b*>) = upper_bound Iab
proof
A5: len <*a,b*> = 2 by FINSEQ_1:44;
upper_bound Iab = b by A1, A2, JORDAN5A:19;
hence <*a,b*> . (len <*a,b*>) = upper_bound Iab by A5, FINSEQ_1:44; :: thesis: verum
end;
hence <*a,b*> is Division of Iab by A3, A4, INTEGRA1:def 2; :: thesis: verum