let X be non empty TopSpace; 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; ( 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
; ( 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 ;
RELAT_1:def 2 ( ( 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 )
( not [x,y] in EqR or [x,y] in EqRel (X,a,b) )proof
assume A3:
[x,y] in EqRel (
X,
a,
b)
;
[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;
verum
end;
assume A5:
[x,y] in EqR
;
[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;
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; verum