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 Z: 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:60;
hence Int A c= Int B by Z, TOPS_1:44, TOPS_1:56; :: according to XBOOLE_0:def 10 :: thesis: Int B c= Int A
reconsider BB = Int B as Subset of T ;
Int B is open ;
then BB is open by XX, PRE_TOPC:60;
hence Int B c= Int A by Z, TOPS_1:44, TOPS_1:56; :: thesis: verum