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 set ; :: 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:48;
P,C are_homotopic by Th2;
then x = Class (EqRel T,a),C by A1, TOPALG_1:47;
hence x in {(Class (EqRel T,a),C)} by TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: 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 5;
hence x in the carrier of (pi_1 T,a) by TOPALG_1:def 5; :: thesis: verum