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