let X be TopStruct ; :: thesis: for X0 being SubSpace of X holds the carrier of X0 is Subset of X
let X0 be SubSpace of X; :: thesis: the carrier of X0 is Subset of X
reconsider A = [#] X0 as Subset of ([#] X) by PRE_TOPC:def 4;
A c= [#] X ;
hence the carrier of X0 is Subset of X ; :: thesis: verum