let a, b be Real; :: thesis: for I being Interval st a in I & b in I holds
[.a,b.] c= I
let I be Interval; :: thesis: ( a in I & b in I implies [.a,b.] c= I )
assume that
A1: a in I and
A2: b in I ; :: thesis: [.a,b.] c= I

per cases ( I is open_interval or I is closed_interval or I is left_open_interval or I is right_open_interval ) by MEASURE5:1;

suppose I is open_interval ; :: thesis: [.a,b.] c= I

then consider p, q being R_eal such that
A3: I = ].p,q.[ by MEASURE5:def 2;
A4: ( p < a & b < q ) by A1, A2, A3, XXREAL_1:4;

now :: thesis: for x being Real st x in [.a,b.] holds
x in I

let x be Real; :: thesis: ( x in [.a,b.] implies x in I )
assume x in [.a,b.] ; :: thesis: x in I
then ( a <= x & x <= b ) by XXREAL_1:1;
then ( p < x & x < q ) by A4, XXREAL_0:2;
hence x in I by A3, XXREAL_1:4; :: thesis: verum

end;

hence [.a,b.] c= I ; :: thesis: verum

end;

suppose I is closed_interval ; :: thesis: [.a,b.] c= I

then consider p, q being Real such that
A5: I = [.p,q.] by MEASURE5:def 3;
A6: ( p <= a & b <= q ) by A1, A2, A5, XXREAL_1:1;

now :: thesis: for x being Real st x in [.a,b.] holds
x in I

let x be Real; :: thesis: ( x in [.a,b.] implies x in I )
assume x in [.a,b.] ; :: thesis: x in I
then ( a <= x & x <= b ) by XXREAL_1:1;
then ( p <= x & x <= q ) by A6, XXREAL_0:2;
hence x in I by A5, XXREAL_1:1; :: thesis: verum

end;

hence [.a,b.] c= I ; :: thesis: verum

end;

suppose I is left_open_interval ; :: thesis: [.a,b.] c= I

then consider p being R_eal, q being Real such that
A7: I = ].p,q.] by MEASURE5:def 5;
A8: ( p < a & b <= q ) by A1, A2, A7, XXREAL_1:2;

now :: thesis: for x being Real st x in [.a,b.] holds
x in I

let x be Real; :: thesis: ( x in [.a,b.] implies x in I )
assume x in [.a,b.] ; :: thesis: x in I
then ( a <= x & x <= b ) by XXREAL_1:1;
then ( p < x & x <= q ) by A8, XXREAL_0:2;
hence x in I by A7, XXREAL_1:2; :: thesis: verum

end;

hence [.a,b.] c= I ; :: thesis: verum

end;

suppose I is right_open_interval ; :: thesis: [.a,b.] c= I

then consider p being Real, q being R_eal such that
A9: I = [.p,q.[ by MEASURE5:def 4;
A10: ( p <= a & b < q ) by A1, A2, A9, XXREAL_1:3;

now :: thesis: for x being Real st x in [.a,b.] holds
x in I

let x be Real; :: thesis: ( x in [.a,b.] implies x in I )
assume x in [.a,b.] ; :: thesis: x in I
then ( a <= x & x <= b ) by XXREAL_1:1;
then ( p <= x & x < q ) by A10, XXREAL_0:2;
hence x in I by A9, XXREAL_1:3; :: thesis: verum

end;

hence [.a,b.] c= I ; :: thesis: verum

end;

end;