let F be Homotopy of P,Q; :: thesis: F is continuous
P,Q are_homotopic by Th59;
hence F is continuous by BORSUK_6:def 11; :: thesis: verum