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

for P being Loop of t holds

( P . 0 = t & P . 1 = t )

let t be Point of T; :: thesis: for P being Loop of t holds

( P . 0 = t & P . 1 = t )

let P be Loop of t; :: thesis: ( P . 0 = t & P . 1 = t )

t,t are_connected ;

hence ( P . 0 = t & P . 1 = t ) by BORSUK_2:def 2; :: thesis: verum

for P being Loop of t holds

( P . 0 = t & P . 1 = t )

let t be Point of T; :: thesis: for P being Loop of t holds

( P . 0 = t & P . 1 = t )

let P be Loop of t; :: thesis: ( P . 0 = t & P . 1 = t )

t,t are_connected ;

hence ( P . 0 = t & P . 1 = t ) by BORSUK_2:def 2; :: thesis: verum