let X be non empty TopSpace; :: thesis: for a, b being Point of X st a,b are_connected holds
( not EqRel (X,a,b) is empty & EqRel (X,a,b) is total & EqRel (X,a,b) is symmetric & EqRel (X,a,b) is transitive )
let a, b be Point of X; :: thesis: ( a,b are_connected implies ( not EqRel (X,a,b) is empty & EqRel (X,a,b) is total & EqRel (X,a,b) is symmetric & EqRel (X,a,b) is transitive ) )
set E = EqRel (X,a,b);
set W = Paths (a,b);
assume A1: a,b are_connected ; :: thesis: ( not EqRel (X,a,b) is empty & EqRel (X,a,b) is total & EqRel (X,a,b) is symmetric & EqRel (X,a,b) is transitive )
then consider EqR being Equivalence_Relation of (Paths (a,b)) such that
A2: for x, y being object holds
( [x,y] in EqR 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 Lm2;
EqRel (X,a,b) = EqR

proof

let x, y be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [x,y] in EqRel (X,a,b) or [x,y] in EqR ) & ( not [x,y] in EqR or [x,y] in EqRel (X,a,b) ) )
thus ( [x,y] in EqRel (X,a,b) implies [x,y] in EqR ) :: thesis: ( not [x,y] in EqR or [x,y] in EqRel (X,a,b) )

proof

assume A3: [x,y] in EqRel (X,a,b) ; :: thesis: [x,y] in EqR
then A4: ( 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 A1, A3, Def3;
hence [x,y] in EqR by A2, A4; :: thesis: verum

end;

assume A5: [x,y] in EqR ; :: thesis: [x,y] in EqRel (X,a,b)
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;
ex P, Q being Path of a,b st
( P = x & Q = y & P,Q are_homotopic ) by A2, A5;
hence [x,y] in EqRel (X,a,b) by A1, Def3; :: thesis: verum

end;

hence ( not EqRel (X,a,b) is empty & EqRel (X,a,b) is total & EqRel (X,a,b) is symmetric & EqRel (X,a,b) is transitive ) by EQREL_1:9, RELAT_1:40; :: thesis: verum