let X be TopStruct ; :: thesis: for Y being SubSpace of X holds the carrier of Y c= the carrier of X
let Y be SubSpace of X; :: thesis: the carrier of Y c= the carrier of X
( the carrier of Y = [#] Y & the carrier of X = [#] X ) ;
hence the carrier of Y c= the carrier of X by PRE_TOPC:def 4; :: thesis: verum