set C = the 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)), the constant Loop of a))} = Class (EqRel ((TOP-REAL n),a)) by Th60;
hence pi_1 ((TOP-REAL n),a) is trivial by Def5; :: thesis: verum