let X be strict TopStruct ; :: thesis: X | ([#] X) = X
reconsider X0 = X as SubSpace of X by Th2;
reconsider P = [#] X0 as Subset of X ;
X | P = X0 by PRE_TOPC:def 5;
hence X | ([#] X) = X ; :: thesis: verum