let a, b be Point of I[01]; :: thesis: ].a,b.[ is Subset of I[01]
A1: [.a,b.] is Subset of I[01] by BORSUK_1:40, XXREAL_2:def 12;
].a,b.[ c= [.a,b.] by XXREAL_1:25;
hence ].a,b.[ is Subset of I[01] by A1, XBOOLE_1:1; :: thesis: verum