let X be non empty TopSpace; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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 :: thesis: ( 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)) ; :: thesis: 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; :: thesis: x = Class ((EqRel (X,a)),P)
thus x = Class ((EqRel (X,a)),P) by A2; :: thesis: verum

end;

given P being Loop of a such that A3: x = Class ((EqRel (X,a)),P) ; :: thesis: 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; :: thesis: verum