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

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