consider E being Equivalence_Relation of (Paths a,b) such that
A2: for x, y being set holds
( [x,y] in E iff ( x in Paths a,b & y in Paths a,b & ex P, Q being Path of a,b st
( P = x & Q = y & P,Q are_homotopic ) ) ) by A1, Lm2;
take E ; :: thesis: for P, Q being Path of a,b holds
( [P,Q] in E iff P,Q are_homotopic )
let P, Q be Path of a,b; :: 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 Path of a,b st
( P1 = P & Q1 = Q & P1,Q1 are_homotopic ) by A2;
hence P,Q are_homotopic ; :: thesis: verum

end;

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