theorem Th22: :: BORSUK_3:22

for X, Y being TopSpace
for Z being Subset of [:Y,X:]
for V being Subset of X
for W being Subset of Y st Z = [:W,V:] holds
TopStruct(# the carrier of [:(Y | W),(X | V):], the topology of [:(Y | W),(X | V):] #) = TopStruct(# the carrier of ([:Y,X:] | Z), the topology of ([:Y,X:] | Z) #)