let f be continuous Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),(TOP-REAL 2); :: thesis: f is with_antipodals
assume A1: not f is with_antipodals ; :: thesis: contradiction
then H₁(f) is not nullhomotopic Loop of (Sn1->Sn f) . c100a by Lm20;
hence contradiction by A1, Lm16; :: thesis: verum