let X be non empty TopSpace; :: thesis: for A being Subset of X
for X0 being non empty SubSpace of X st the carrier of X0 misses A holds
for x0 being Point of X0 holds (modid (X,A)) | X0 is_continuous_at x0
let A be Subset of X; :: thesis: for X0 being non empty SubSpace of X st the carrier of X0 misses A holds
for x0 being Point of X0 holds (modid (X,A)) | X0 is_continuous_at x0
let X0 be non empty SubSpace of X; :: thesis: ( the carrier of X0 misses A implies for x0 being Point of X0 holds (modid (X,A)) | X0 is_continuous_at x0 )
assume A1: the carrier of X0 /\ A = {} ; :: according to XBOOLE_0:def 7 :: thesis: for x0 being Point of X0 holds (modid (X,A)) | X0 is_continuous_at x0
let x0 be Point of X0; :: thesis: (modid (X,A)) | X0 is_continuous_at x0
( x0 in the carrier of X0 & the carrier of X0 c= the carrier of X ) by BORSUK_1:1;
then reconsider x = x0 as Point of X ;
not x in A by A1, XBOOLE_0:def 4;
hence (modid (X,A)) | X0 is_continuous_at x0 by Th58, Th96; :: thesis: verum