let T be TopStruct ; :: thesis: for X being Subset of T
for Y being Subset of TopStruct(# the carrier of T,the topology of T #) st X = Y holds
TopStruct(# the carrier of (T | X),the topology of (T | X) #) = TopStruct(# the carrier of T,the topology of T #) | Y
let X be Subset of T; :: thesis: for Y being Subset of TopStruct(# the carrier of T,the topology of T #) st X = Y holds
TopStruct(# the carrier of (T | X),the topology of (T | X) #) = TopStruct(# the carrier of T,the topology of T #) | Y
let Y be Subset of TopStruct(# the carrier of T,the topology of T #); :: thesis: ( X = Y implies TopStruct(# the carrier of (T | X),the topology of (T | X) #) = TopStruct(# the carrier of T,the topology of T #) | Y )
assume X = Y ; :: thesis: TopStruct(# the carrier of (T | X),the topology of (T | X) #) = TopStruct(# the carrier of T,the topology of T #) | Y
then A1: [#] TopStruct(# the carrier of (T | X),the topology of (T | X) #) = Y by Def10;
TopStruct(# the carrier of (T | X),the topology of (T | X) #) is strict SubSpace of TopStruct(# the carrier of T,the topology of T #) by Th65;
hence TopStruct(# the carrier of (T | X),the topology of (T | X) #) = TopStruct(# the carrier of T,the topology of T #) | Y by A1, Def10; :: thesis: verum