let X, Y, X1, Y1 be TopSpace; :: thesis: ( TopStruct(# the carrier of X,the topology of X #) = TopStruct(# the carrier of X1,the topology of X1 #) & TopStruct(# the carrier of Y,the topology of Y #) = TopStruct(# the carrier of Y1,the topology of Y1 #) implies [:X,Y:] = [:X1,Y1:] )
assume A1: ( TopStruct(# the carrier of X,the topology of X #) = TopStruct(# the carrier of X1,the topology of X1 #) & TopStruct(# the carrier of Y,the topology of Y #) = TopStruct(# the carrier of Y1,the topology of Y1 #) ) ; :: thesis: [:X,Y:] = [:X1,Y1:]
A2: the carrier of [:X,Y:] = [:the carrier of X,the carrier of Y:] by BORSUK_1:def 5
.= the carrier of [:X1,Y1:] by A1, BORSUK_1:def 5 ;
set U2 = { (union A) where A is Subset-Family of [:X1,Y1:] : A c= { [:X2,Y2:] where X2 is Subset of X1, Y2 is Subset of Y1 : ( X2 in the topology of X1 & Y2 in the topology of Y1 ) } } ;
the topology of [:X,Y:] = { (union A) where A is Subset-Family of [:X1,Y1:] : A c= { [:X2,Y2:] where X2 is Subset of X1, Y2 is Subset of Y1 : ( X2 in the topology of X1 & Y2 in the topology of Y1 ) } } by A1, A2, BORSUK_1:def 5
.= the topology of [:X1,Y1:] by BORSUK_1:def 5 ;
hence [:X,Y:] = [:X1,Y1:] by A2; :: thesis: verum