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