let X be non empty TopSpace; for a being Point of X
for x being set holds
( x in the carrier of (pi_1 (X,a)) iff ex P being Loop of a st x = Class ((EqRel (X,a)),P) )
let a be Point of X; for x being set holds
( x in the carrier of (pi_1 (X,a)) iff ex P being Loop of a st x = Class ((EqRel (X,a)),P) )
let x be set ; ( x in the carrier of (pi_1 (X,a)) iff ex P being Loop of a st x = Class ((EqRel (X,a)),P) )
A1:
the carrier of (pi_1 (X,a)) = Class (EqRel (X,a))
by Def5;
hereby ( ex P being Loop of a st x = Class ((EqRel (X,a)),P) implies x in the carrier of (pi_1 (X,a)) )
assume
x in the
carrier of
(pi_1 (X,a))
;
ex P being Loop of a st x = Class ((EqRel (X,a)),P)then consider P being
Element of
Loops a such that A2:
x = Class (
(EqRel (X,a)),
P)
by A1, EQREL_1:36;
reconsider P =
P as
Loop of
a by Def1;
take P =
P;
x = Class ((EqRel (X,a)),P)thus
x = Class (
(EqRel (X,a)),
P)
by A2;
verum
end;
given P being Loop of a such that A3:
x = Class ((EqRel (X,a)),P)
; x in the carrier of (pi_1 (X,a))
P in Loops a
by Def1;
hence
x in the carrier of (pi_1 (X,a))
by A1, A3, EQREL_1:def 3; verum