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 ; :: 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