let a, b be Real; :: thesis: for Iab being non empty closed_interval Subset of REAL st Iab = [.a,b.] holds
<*b*> is Division of Iab
let Iab be non empty closed_interval Subset of REAL; :: thesis: ( Iab = [.a,b.] implies <*b*> is Division of Iab )
assume A1: Iab = [.a,b.] ; :: thesis: <*b*> is Division of Iab
A2: a <= b by A1, XXREAL_1:29;
set D = <*b*>;
A3: rng <*b*> c= Iab

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng <*b*> or x in Iab )
assume x in rng <*b*> ; :: thesis: x in Iab
then x in {b} by FINSEQ_1:39;
then x = b by TARSKI:def 1;
hence x in Iab by A1, A2, XXREAL_1:1; :: thesis: verum

end;

<*b*> . (len <*b*>) = upper_bound Iab

proof

dom <*b*> = Seg 1 by FINSEQ_1:def 8;
then <*b*> . (len <*b*>) = <*b*> . 1 by FINSEQ_1:def 3
.= b ;
hence <*b*> . (len <*b*>) = upper_bound Iab by A1, A2, JORDAN5A:19; :: thesis: verum

end;

hence <*b*> is Division of Iab by A3, INTEGRA1:def 2; :: thesis: verum