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

take X modified_with_respect_to B ; :: thesis: for A being Subset of X st A = the carrier of X0 holds

X modified_with_respect_to B = X modified_with_respect_to A

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

X modified_with_respect_to B = X modified_with_respect_to A ; :: thesis: verum

take X modified_with_respect_to B ; :: thesis: for A being Subset of X st A = the carrier of X0 holds

X modified_with_respect_to B = X modified_with_respect_to A

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

X modified_with_respect_to B = X modified_with_respect_to A ; :: thesis: verum