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