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