theorem :: BORSUK_4:18

for p1, p2 being Point of I[01] holds [.p1,p2.] is Subset of I[01] by BORSUK_1:40, XXREAL_2:def 12;