let n be Nat; 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); 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; 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 TARSKI:def 3,
XBOOLE_0:def 10 {(Class ((EqRel ((TOP-REAL n),a)),C))} c= the carrier of (pi_1 ((TOP-REAL n),a))
let x be
object ;
( 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))
;
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;
verum
end;
let x be object ; TARSKI:def 3 ( 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))}
; 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; verum