let n be Nat; :: thesis: for a being Point of (TOP-REAL n)
for C being Loop of a holds the carrier of (pi_1 ((TOP-REAL n),a)) = {(Class ((EqRel ((TOP-REAL n),a)),C))}
let a be Point of (TOP-REAL n); :: thesis: for C being Loop of a holds the carrier of (pi_1 ((TOP-REAL n),a)) = {(Class ((EqRel ((TOP-REAL n),a)),C))}
let C be Loop of a; :: thesis: the carrier of (pi_1 ((TOP-REAL n),a)) = {(Class ((EqRel ((TOP-REAL n),a)),C))}
set X = TOP-REAL n;
set E = EqRel ((TOP-REAL n),a);

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

let x be object ; :: thesis: ( x in the carrier of (pi_1 ((TOP-REAL n),a)) implies x in {(Class ((EqRel ((TOP-REAL n),a)),C))} )
assume x in the carrier of (pi_1 ((TOP-REAL n),a)) ; :: thesis: x in {(Class ((EqRel ((TOP-REAL n),a)),C))}
then consider P being Loop of a such that
A1: x = Class ((EqRel ((TOP-REAL n),a)),P) by Th47;
P,C are_homotopic by Th59;
then x = Class ((EqRel ((TOP-REAL n),a)),C) by A1, Th46;
hence x in {(Class ((EqRel ((TOP-REAL n),a)),C))} by TARSKI:def 1; :: thesis: verum

end;

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