consider E being Equivalence_Relation of (Loops a) such that
A1: for x, y being set holds
( [x,y] in E 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;
take E ; :: thesis: for P, Q being Loop of a holds
( [P,Q] in E iff P,Q are_homotopic )
let P, Q be Loop of a; :: thesis: ( [P,Q] in E iff P,Q are_homotopic )
thus ( [P,Q] in E implies P,Q are_homotopic ) :: thesis: ( P,Q are_homotopic implies [P,Q] in E )

proof

assume [P,Q] in E ; :: thesis: P,Q are_homotopic
then ex P1, Q1 being Loop of a st
( P1 = P & Q1 = Q & P1,Q1 are_homotopic ) by A1;
hence P,Q are_homotopic ; :: thesis: verum

end;

( P in Loops a & Q in Loops a ) by Def1;
hence ( P,Q are_homotopic implies [P,Q] in E ) by A1; :: thesis: verum