let P be Point of I[01] ; :: thesis: P is Real
P in [.0 ,1.] by BORSUK_1:83;
hence P is Real ; :: thesis: verum