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. )
per cases ( a = b or b < a ) by A3, XXREAL_0:1;
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;
suppose b < a ; :: thesis: ( diameter A = 0. & diameter B = 0. )
then A6: B = {} by A2, XXREAL_1:29;
then A = {} by A1;
hence ( diameter A = 0. & diameter B = 0. ) by A6, Def6; :: thesis: verum
end;
end;