set C = the constant Loop of a;
set E = EqRel (T,a);
the carrier of (pi_1 (T,a)) = Class (EqRel (T,a)) by TOPALG_1:def 5;
then {(Class ((EqRel (T,a)), the constant Loop of a))} = Class (EqRel (T,a)) by Th3;
hence pi_1 (T,a) is trivial by TOPALG_1:def 5; :: thesis: verum