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