let T be TopSpace; :: thesis: for A being Subset of T
for B being Subset of TopStruct(# the carrier of T, the topology of T #) st A = B holds
Int A = Int B
let A be Subset of T; :: thesis: for B being Subset of TopStruct(# the carrier of T, the topology of T #) st A = B holds
Int A = Int B
let B be Subset of TopStruct(# the carrier of T, the topology of T #); :: thesis: ( A = B implies Int A = Int B )
assume A1: A = B ; :: thesis: Int A = Int B
reconsider AA = Int A as Subset of TopStruct(# the carrier of T, the topology of T #) ;
AA is open by PRE_TOPC:30;
hence Int A c= Int B by A1, TOPS_1:16, TOPS_1:24; :: according to XBOOLE_0:def 10 :: thesis: Int B c= Int A
reconsider BB = Int B as Subset of T ;
BB is open by PRE_TOPC:30;
hence Int B c= Int A by A1, TOPS_1:16, TOPS_1:24; :: thesis: verum