let n be Element of NAT ; :: thesis: for T being non empty convex SubSpace of TOP-REAL n
for a being Point of T
for C being Loop of a holds the carrier of (pi_1 (T,a)) = {(Class ((EqRel (T,a)),C))}
let T be non empty convex SubSpace of TOP-REAL n; :: thesis: for a being Point of T
for C being Loop of a holds the carrier of (pi_1 (T,a)) = {(Class ((EqRel (T,a)),C))}
let a be Point of T; :: thesis: for C being Loop of a holds the carrier of (pi_1 (T,a)) = {(Class ((EqRel (T,a)),C))}
let C be Loop of a; :: thesis: the carrier of (pi_1 (T,a)) = {(Class ((EqRel (T,a)),C))}
set E = EqRel (T,a);

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {(Class ((EqRel (T,a)),C))} c= the carrier of (pi_1 (T,a))

let x be object ; :: thesis: ( x in the carrier of (pi_1 (T,a)) implies x in {(Class ((EqRel (T,a)),C))} )
assume x in the carrier of (pi_1 (T,a)) ; :: thesis: x in {(Class ((EqRel (T,a)),C))}
then consider P being Loop of a such that
A1: x = Class ((EqRel (T,a)),P) by TOPALG_1:47;
P,C are_homotopic by Th2;
then x = Class ((EqRel (T,a)),C) by A1, TOPALG_1:46;
hence x in {(Class ((EqRel (T,a)),C))} by TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(Class ((EqRel (T,a)),C))} or x in the carrier of (pi_1 (T,a)) )
assume x in {(Class ((EqRel (T,a)),C))} ; :: thesis: x in the carrier of (pi_1 (T,a))
then A2: x = Class ((EqRel (T,a)),C) by TARSKI:def 1;
C in Loops a by TOPALG_1:def 1;
then x in Class (EqRel (T,a)) by A2, EQREL_1:def 3;
hence x in the carrier of (pi_1 (T,a)) by TOPALG_1:def 5; :: thesis: verum