let X, Y be TopSpace; :: thesis: 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) #)
let Z be Subset of [:Y,X:]; :: thesis: 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) #)
let V be Subset of X; :: thesis: 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) #)
let W be Subset of Y; :: thesis: ( Z = [:W,V:] implies 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) #) )
reconsider A = [:(Y | W),(X | V):] as SubSpace of [:Y,X:] by Th21;
assume A1: Z = [:W,V:] ; :: thesis: 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) #)
the carrier of A = [: the carrier of (Y | W), the carrier of (X | V):] by BORSUK_1:def 2
.= [: the carrier of (Y | W),V:] by PRE_TOPC:8
.= Z by A1, PRE_TOPC:8
.= the carrier of ([:Y,X:] | Z) by PRE_TOPC:8 ;
then ( A is SubSpace of [:Y,X:] | Z & [:Y,X:] | Z is SubSpace of A ) by TOPMETR:3;
hence 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) #) by TSEP_1:6; :: thesis: verum