set E = EqRel X,a;
consider EqR being Equivalence_Relation of Loops a such that
A1: for x, y being set holds
( [x,y] in EqR iff ( x in Loops a & y in Loops a & ex P, Q being Loop of a st
( P = x & Q = y & P,Q are_homotopic ) ) ) by Lm2;
EqRel X,a = EqR

proof

let x, y be set ; :: according to RELAT_1:def 2 :: thesis: ( ( not [x,y] in EqRel X,a or [x,y] in EqR ) & ( not [x,y] in EqR or [x,y] in EqRel X,a ) )
thus ( [x,y] in EqRel X,a implies [x,y] in EqR ) :: thesis: ( not [x,y] in EqR or [x,y] in EqRel X,a )

proof

assume A2: [x,y] in EqRel X,a ; :: thesis: [x,y] in EqR
then A3: ( x in Loops a & y in Loops a ) by ZFMISC_1:106;
then reconsider x = x, y = y as Loop of a by Def1;
x,y are_homotopic by A2, Def2;
hence [x,y] in EqR by A1, A3; :: thesis: verum

end;

assume A4: [x,y] in EqR ; :: thesis: [x,y] in EqRel X,a
then ( x in Loops a & y in Loops a ) by ZFMISC_1:106;
then reconsider x = x, y = y as Loop of a by Def1;
ex P, Q being Loop of a st
( P = x & Q = y & P,Q are_homotopic ) by A1, A4;
hence [x,y] in EqRel X,a by Def2; :: thesis: verum

end;

hence ( not EqRel X,a is empty & EqRel X,a is total & EqRel X,a is symmetric & EqRel X,a is transitive ) by EQREL_1:16, RELAT_1:63; :: thesis: verum