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