let GX be TopStruct ; :: thesis: for A being Subset of holds the carrier of (GX | A) = A
let A be Subset of ; :: thesis: the carrier of (GX | A) = A
A = [#] (GX | A) by Def10;
hence the carrier of (GX | A) = A ; :: thesis: verum