consider C being 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),C)} = Class (EqRel T,a) by Th3;
hence pi_1 T,a is trivial by TOPALG_1:def 5; :: thesis: verum