let T be non empty strict TopSpace; :: thesis: for A being Subset of T holds Int A = Int (Top2NTop A)
let A be Subset of T; :: thesis: Int A = Int (Top2NTop A)
reconsider NT = Top2NTop T as NTopSpace ;
reconsider NA = Top2NTop A as Subset of NT ;

now :: thesis: ( Int NA c= Int A & Int A c= Int NA )

now :: thesis: for o being object st o in Int NA holds
o in Int A

let o be object ; :: thesis: ( o in Int NA implies o in Int A )
assume A1: o in Int NA ; :: thesis: o in Int A
then reconsider x = o as Point of NT ;
consider y being Point of NT such that
A2: x = y and
A3: y is_interior_point_of NA by A1;
consider NO being open Subset of NT such that
A4: y in NO and
A5: NO c= NA by A3, Lm4;
reconsider y9 = NTop2Top y as Point of T by FINTOPO7:24;
reconsider O = NO as open Subset of (NTop2Top NT) by Lm9;
NTop2Top NT = T by FINTOPO7:24;
then reconsider O = O as open Subset of T ;
( y9 in O & O c= A ) by A4, A5;
then A is a_neighborhood of y9 by URYSOHN1:def 6;
hence o in Int A by CONNSP_2:def 1, A2; :: thesis: verum

end;

hence Int NA c= Int A ; :: thesis: Int A c= Int NA

now :: thesis: for o being object st o in Int A holds
o in Int NA

let o be object ; :: thesis: ( o in Int A implies o in Int NA )
assume A6: o in Int A ; :: thesis: o in Int NA
then reconsider x = o as Point of T ;
consider O being Subset of T such that
A7: O is open and
A8: x in O and
A9: O c= A by A6, CONNSP_2:def 1, URYSOHN1:def 6;
reconsider y = Top2NTop x as Point of NT ;
reconsider NO = O as open Subset of NT by A7, Lm1;
( y in NO & NO c= NA ) by A8, A9;
then y is_interior_point_of NA by Lm4;
hence o in Int NA ; :: thesis: verum

end;

hence Int A c= Int NA ; :: thesis: verum

end;

hence Int A = Int (Top2NTop A) ; :: thesis: verum