theorem :: TOPALG_2:17

for x being Point of I[01]
for C being Loop of x holds the carrier of (pi_1 (I[01],x)) = {(Class ((EqRel (I[01],x)),C))} by Th10, Th13;