let a, b, c be Real; for Iab, Iac, Icb being non empty compact Subset of REAL st a <= c & c <= b & Iab = [.a,b.] & Iac = [.a,c.] & Icb = [.c,b.] holds
for Dac being Division of Iac
for Dcb being Division of Icb st c < Dcb . 1 holds
Dac ^ Dcb is Division of Iab
let Iab, Iac, Icb be non empty compact Subset of REAL; ( a <= c & c <= b & Iab = [.a,b.] & Iac = [.a,c.] & Icb = [.c,b.] implies for Dac being Division of Iac
for Dcb being Division of Icb st c < Dcb . 1 holds
Dac ^ Dcb is Division of Iab )
assume that
A1:
( a <= c & c <= b )
and
A2:
Iab = [.a,b.]
and
A3:
Iac = [.a,c.]
and
A4:
Icb = [.c,b.]
; for Dac being Division of Iac
for Dcb being Division of Icb st c < Dcb . 1 holds
Dac ^ Dcb is Division of Iab
let Dac be Division of Iac; for Dcb being Division of Icb st c < Dcb . 1 holds
Dac ^ Dcb is Division of Iab
let Dcb be Division of Icb; ( c < Dcb . 1 implies Dac ^ Dcb is Division of Iab )
assume A5:
c < Dcb . 1
; Dac ^ Dcb is Division of Iab
set Dacb = Dac ^ Dcb;
for e1, e2 being ExtReal st e1 in dom (Dac ^ Dcb) & e2 in dom (Dac ^ Dcb) & e1 < e2 holds
(Dac ^ Dcb) . e1 < (Dac ^ Dcb) . e2
proof
let e1,
e2 be
ExtReal;
( e1 in dom (Dac ^ Dcb) & e2 in dom (Dac ^ Dcb) & e1 < e2 implies (Dac ^ Dcb) . e1 < (Dac ^ Dcb) . e2 )
assume that A6:
e1 in dom (Dac ^ Dcb)
and A7:
e2 in dom (Dac ^ Dcb)
and A8:
e1 < e2
;
(Dac ^ Dcb) . e1 < (Dac ^ Dcb) . e2
end;
then A23:
Dac ^ Dcb is increasing
;
A24:
rng (Dac ^ Dcb) c= Iab
proof
let x be
object ;
TARSKI:def 3 ( not x in rng (Dac ^ Dcb) or x in Iab )
assume A25:
x in rng (Dac ^ Dcb)
;
x in Iab
A26:
rng Dac c= [.a,c.]
by A3, INTEGRA1:def 2;
rng Dcb c= [.c,b.]
by A4, INTEGRA1:def 2;
then
(rng Dac) \/ (rng Dcb) c= [.a,c.] \/ [.c,b.]
by XBOOLE_1:13, A26;
then
rng (Dac ^ Dcb) c= [.a,c.] \/ [.c,b.]
by FINSEQ_1:31;
then
rng (Dac ^ Dcb) c= [.a,b.]
by A1, XXREAL_1:165;
hence
x in Iab
by A25, A2;
verum
end;
(Dac ^ Dcb) . (len (Dac ^ Dcb)) = upper_bound Iab
hence
Dac ^ Dcb is Division of Iab
by A23, A24, INTEGRA1:def 2; verum