[#] X0 c= [#] X by PRE_TOPC:def 4;
then reconsider O = [#] X0 as Subset of X ;
X modified_with_respect_to X0 = X modified_with_respect_to O by Def10;
hence not X modified_with_respect_to X0 is empty ; :: thesis: verum