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 A1: ( ( 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 ) ) ; :: thesis: Y1 = Y2
reconsider C = the carrier of X0 as Subset of X by TSEP_1:1;
( Y1 = X modified_with_respect_to C & Y2 = X modified_with_respect_to C ) by A1;
hence Y1 = Y2 ; :: thesis: verum