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:45;
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 5; :: thesis: verum