consider C being constant Loop of a;
set X = TOP-REAL n;
set E = EqRel (TOP-REAL n),a;
the carrier of (pi_1 (TOP-REAL n),a) = Class (EqRel (TOP-REAL n),a) by Def5;
then {(Class (EqRel (TOP-REAL n),a),C)} = Class (EqRel (TOP-REAL n),a) by Th61;
hence pi_1 (TOP-REAL n),a is trivial by Def5; :: thesis: verum