let T be non empty TopSpace; :: thesis: for t being Point of T

for x being Point of I[01]

for P being constant Loop of t holds P . x = t

let t be Point of T; :: thesis: for x being Point of I[01]

for P being constant Loop of t holds P . x = t

let x be Point of I[01]; :: thesis: for P being constant Loop of t holds P . x = t

let P be constant Loop of t; :: thesis: P . x = t

P = I[01] --> t by BORSUK_2:5;

hence P . x = t ; :: thesis: verum

for x being Point of I[01]

for P being constant Loop of t holds P . x = t

let t be Point of T; :: thesis: for x being Point of I[01]

for P being constant Loop of t holds P . x = t

let x be Point of I[01]; :: thesis: for P being constant Loop of t holds P . x = t

let P be constant Loop of t; :: thesis: P . x = t

P = I[01] --> t by BORSUK_2:5;

hence P . x = t ; :: thesis: verum