consider E being Equivalence_Relation of (Paths (a,b)) such that
A2:
for x, y being object 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
; 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; ( [P,Q] in E iff P,Q are_homotopic )
thus
( [P,Q] in E implies P,Q are_homotopic )
( P,Q are_homotopic implies [P,Q] in E )
( P in Paths (a,b) & Q in Paths (a,b) )
by Def1;
hence
( P,Q are_homotopic implies [P,Q] in E )
by A2; verum