let T be non empty TopStruct ; :: thesis: for t1, t2 being Point of T
for p being Path of t1,t2 holds
( inf (dom p) = 0 & sup (dom p) = 1 )
let t1, t2 be Point of T; :: thesis: for p being Path of t1,t2 holds
( inf (dom p) = 0 & sup (dom p) = 1 )
let p be Path of t1,t2; :: thesis: ( inf (dom p) = 0 & sup (dom p) = 1 )
[.0,1.] = dom p by BORSUK_1:40, FUNCT_2:def 1;
hence ( inf (dom p) = 0 & sup (dom p) = 1 ) by XXREAL_2:25, XXREAL_2:29; :: thesis: verum