reconsider C = the carrier of X0 as Subset of X by TSEP_1:1;

let Y1, Y2 be strict TopSpace; :: thesis: ( ( for A being Subset of X st A = the carrier of X0 holds

Y1 = X modified_with_respect_to A ) & ( for A being Subset of X st A = the carrier of X0 holds

Y2 = X modified_with_respect_to A ) implies Y1 = Y2 )

assume that

A1: for A being Subset of X st A = the carrier of X0 holds

Y1 = X modified_with_respect_to A and

A2: for A being Subset of X st A = the carrier of X0 holds

Y2 = X modified_with_respect_to A ; :: thesis: Y1 = Y2

Y1 = X modified_with_respect_to C by A1;

hence Y1 = Y2 by A2; :: thesis: verum

let Y1, Y2 be strict TopSpace; :: thesis: ( ( for A being Subset of X st A = the carrier of X0 holds

Y1 = X modified_with_respect_to A ) & ( for A being Subset of X st A = the carrier of X0 holds

Y2 = X modified_with_respect_to A ) implies Y1 = Y2 )

assume that

A1: for A being Subset of X st A = the carrier of X0 holds

Y1 = X modified_with_respect_to A and

A2: for A being Subset of X st A = the carrier of X0 holds

Y2 = X modified_with_respect_to A ; :: thesis: Y1 = Y2

Y1 = X modified_with_respect_to C by A1;

hence Y1 = Y2 by A2; :: thesis: verum