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