let a, b be R_eal; :: thesis: for A, B being Interval st A c= B & B = [.a,b.] & b <= a holds

( diameter A = 0. & diameter B = 0. )

let A, B be Interval; :: thesis: ( A c= B & B = [.a,b.] & b <= a implies ( diameter A = 0. & diameter B = 0. ) )

assume that

A1: A c= B and

A2: B = [.a,b.] and

A3: b <= a ; :: thesis: ( diameter A = 0. & diameter B = 0. )

( diameter A = 0. & diameter B = 0. )

let A, B be Interval; :: thesis: ( A c= B & B = [.a,b.] & b <= a implies ( diameter A = 0. & diameter B = 0. ) )

assume that

A1: A c= B and

A2: B = [.a,b.] and

A3: b <= a ; :: thesis: ( diameter A = 0. & diameter B = 0. )

per cases
( a = b or b < a )
by A3, XXREAL_0:1;

end;

suppose A4:
a = b
; :: thesis: ( diameter A = 0. & diameter B = 0. )

then
B = {a}
by A2, XXREAL_1:17;

then ( inf B = a & sup B = a ) by XXREAL_2:11, XXREAL_2:13;

then A5: diameter B = a - a by A2, A4, Def6

.= 0 by XXREAL_3:7 ;

then diameter A <= 0 by A1, Lm2;

hence ( diameter A = 0. & diameter B = 0. ) by A5, Lm1; :: thesis: verum

end;then ( inf B = a & sup B = a ) by XXREAL_2:11, XXREAL_2:13;

then A5: diameter B = a - a by A2, A4, Def6

.= 0 by XXREAL_3:7 ;

then diameter A <= 0 by A1, Lm2;

hence ( diameter A = 0. & diameter B = 0. ) by A5, Lm1; :: thesis: verum