let X be non empty TopStruct ; :: thesis: for A0 being non empty Subset of X ex X0 being non empty strict SubSpace of X st A0 = the carrier of X0
let A0 be non empty Subset of X; :: thesis: ex X0 being non empty strict SubSpace of X st A0 = the carrier of X0
take X0 = X | A0; :: thesis: A0 = the carrier of X0
A0 = [#] X0 by PRE_TOPC:def 5;
hence A0 = the carrier of X0 ; :: thesis: verum