let T be non empty TopSpace; for S being non empty SubSpace of T
for t1, t2 being Point of T
for s1, s2 being Point of S
for A, B being Path of t1,t2
for C, D being Path of s1,s2 st s1,s2 are_connected & t1,t2 are_connected & A = C & B = D & Class ((EqRel (S,s1,s2)),C) = Class ((EqRel (S,s1,s2)),D) holds
Class ((EqRel (T,t1,t2)),A) = Class ((EqRel (T,t1,t2)),B)
let S be non empty SubSpace of T; for t1, t2 being Point of T
for s1, s2 being Point of S
for A, B being Path of t1,t2
for C, D being Path of s1,s2 st s1,s2 are_connected & t1,t2 are_connected & A = C & B = D & Class ((EqRel (S,s1,s2)),C) = Class ((EqRel (S,s1,s2)),D) holds
Class ((EqRel (T,t1,t2)),A) = Class ((EqRel (T,t1,t2)),B)
let t1, t2 be Point of T; for s1, s2 being Point of S
for A, B being Path of t1,t2
for C, D being Path of s1,s2 st s1,s2 are_connected & t1,t2 are_connected & A = C & B = D & Class ((EqRel (S,s1,s2)),C) = Class ((EqRel (S,s1,s2)),D) holds
Class ((EqRel (T,t1,t2)),A) = Class ((EqRel (T,t1,t2)),B)
let s1, s2 be Point of S; for A, B being Path of t1,t2
for C, D being Path of s1,s2 st s1,s2 are_connected & t1,t2 are_connected & A = C & B = D & Class ((EqRel (S,s1,s2)),C) = Class ((EqRel (S,s1,s2)),D) holds
Class ((EqRel (T,t1,t2)),A) = Class ((EqRel (T,t1,t2)),B)
let A, B be Path of t1,t2; for C, D being Path of s1,s2 st s1,s2 are_connected & t1,t2 are_connected & A = C & B = D & Class ((EqRel (S,s1,s2)),C) = Class ((EqRel (S,s1,s2)),D) holds
Class ((EqRel (T,t1,t2)),A) = Class ((EqRel (T,t1,t2)),B)
let C, D be Path of s1,s2; ( s1,s2 are_connected & t1,t2 are_connected & A = C & B = D & Class ((EqRel (S,s1,s2)),C) = Class ((EqRel (S,s1,s2)),D) implies Class ((EqRel (T,t1,t2)),A) = Class ((EqRel (T,t1,t2)),B) )
assume that
A1:
s1,s2 are_connected
and
A2:
t1,t2 are_connected
and
A3:
( A = C & B = D )
; ( not Class ((EqRel (S,s1,s2)),C) = Class ((EqRel (S,s1,s2)),D) or Class ((EqRel (T,t1,t2)),A) = Class ((EqRel (T,t1,t2)),B) )
assume
Class ((EqRel (S,s1,s2)),C) = Class ((EqRel (S,s1,s2)),D)
; Class ((EqRel (T,t1,t2)),A) = Class ((EqRel (T,t1,t2)),B)
then
C,D are_homotopic
by A1, TOPALG_1:46;
then
A,B are_homotopic
by A1, A2, A3, Th6;
hence
Class ((EqRel (T,t1,t2)),A) = Class ((EqRel (T,t1,t2)),B)
by A2, TOPALG_1:46; verum