let E, F be Relation of (Paths (a,b)); :: thesis: ( ( for P, Q being Path of a,b holds
( [P,Q] in E iff P,Q are_homotopic ) ) & ( for P, Q being Path of a,b holds
( [P,Q] in F iff P,Q are_homotopic ) ) implies E = F )
assume that
A3: for P, Q being Path of a,b holds
( [P,Q] in E iff P,Q are_homotopic ) and
A4: for P, Q being Path of a,b holds
( [P,Q] in F iff P,Q are_homotopic ) ; :: thesis: E = F
let x, y be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [x,y] in E or [x,y] in F ) & ( not [x,y] in F or [x,y] in E ) )
thus ( [x,y] in E implies [x,y] in F ) :: thesis: ( not [x,y] in F or [x,y] in E )

proof

assume A5: [x,y] in E ; :: thesis: [x,y] in F
then ( x in Paths (a,b) & y in Paths (a,b) ) by ZFMISC_1:87;
then reconsider x = x, y = y as Path of a,b by Def1;
x,y are_homotopic by A3, A5;
hence [x,y] in F by A4; :: thesis: verum

end;

assume A6: [x,y] in F ; :: thesis: [x,y] in E
then ( x in Paths (a,b) & y in Paths (a,b) ) by ZFMISC_1:87;
then reconsider x = x, y = y as Path of a,b by Def1;
x,y are_homotopic by A4, A6;
hence [x,y] in E by A3; :: thesis: verum