[#] 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

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