let T be non empty TopSpace; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: ( 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) ; :: thesis: 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; :: thesis: verum

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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: ( 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) ; :: thesis: 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; :: thesis: verum