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