let X1, X2 be TopSpace; :: thesis: for D1 being Subset of X1
for D2 being Subset of X2 st D1 = D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is open holds
D2 is open
let D1 be Subset of X1; :: thesis: for D2 being Subset of X2 st D1 = D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is open holds
D2 is open
let D2 be Subset of X2; :: thesis: ( D1 = D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is open implies D2 is open )
assume A1: D1 = D2 ; :: thesis: ( not TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) or not D1 is open or D2 is open )
assume A2: TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) ; :: thesis: ( not D1 is open or D2 is open )
assume D1 in the topology of X1 ; :: according to PRE_TOPC:def 2 :: thesis: D2 is open
hence D2 is open by A1, A2, PRE_TOPC:def 2; :: thesis: verum