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 Def3;
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),Pthen 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),Pthus
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