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 #) holds
Int D1 = Int D2
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 #) holds
Int D1 = Int D2
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 #) implies Int D1 = Int D2 )
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 Int D1 = Int D2 )
A2: Int D1 c= D1 by TOPS_1:16;
then reconsider C2 = Int D1 as Subset of X2 by A1, XBOOLE_1:1;
assume A3: TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) ; :: thesis: Int D1 = Int D2
then A4: C2 c= Int D2 by A1, A2, Th76, TOPS_1:24;
A5: Int D2 c= D2 by TOPS_1:16;
then reconsider C1 = Int D2 as Subset of X1 by A1, XBOOLE_1:1;
C1 c= Int D1 by A1, A3, A5, Th76, TOPS_1:24;
hence Int D1 = Int D2 by A4; :: thesis: verum