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 set ; :: 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 Th48;
P,C are_homotopic by Th60;
then x = Class (EqRel (TOP-REAL n),a),C by A1, Th47;
hence x in {(Class (EqRel (TOP-REAL n),a),C)} by TARSKI:def 1; :: thesis: verum

end;

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