let E, F be Relation of (Loops a); :: thesis: ( ( for P, Q being Loop of a holds
( [P,Q] in E iff P,Q are_homotopic ) ) & ( for P, Q being Loop of a holds
( [P,Q] in F iff P,Q are_homotopic ) ) implies E = F )
assume that
A2: for P, Q being Loop of a holds
( [P,Q] in E iff P,Q are_homotopic ) and
A3: for P, Q being Loop of a holds
( [P,Q] in F iff P,Q are_homotopic ) ; :: thesis: E = F
let x, y be set ; :: 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 A4: [x,y] in E ; :: thesis: [x,y] in F
then ( x in Loops a & y in Loops a ) by ZFMISC_1:106;
then reconsider x = x, y = y as Loop of a by Def1;
x,y are_homotopic by A2, A4;
hence [x,y] in F by A3; :: thesis: verum

end;

assume A5: [x,y] in F ; :: thesis: [x,y] in E
then ( x in Loops a & y in Loops a ) by ZFMISC_1:106;
then reconsider x = x, y = y as Loop of a by Def1;
x,y are_homotopic by A3, A5;
hence [x,y] in E by A2; :: thesis: verum