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 set 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 set ; :: 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:106;
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:106;
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:16, RELAT_1:63; :: thesis: verum