let NT be NTopSpace; :: thesis: for A being Subset of NT holds Int A = Int (NTop2Top A)
let A be Subset of NT; :: thesis: Int A = Int (NTop2Top A)
set NA = A;
reconsider T = NTop2Top NT as non empty TopSpace ;
reconsider A9 = NTop2Top A as Subset of T ;
now :: thesis: ( Int A c= Int A9 & Int A9 c= Int A )
now :: thesis: for o being object st o in Int A holds
o in Int A9
let o be object ; :: thesis: ( o in Int A implies o in Int A9 )
assume o in Int A ; :: thesis: o in Int A9
then consider y being Point of NT such that
A1: o = y and
A2: y is_interior_point_of A ;
consider NO being open Subset of NT such that
A3: y in NO and
A4: NO c= A by A2, Lm4;
reconsider O = NO as open Subset of T by Lm9;
y in O by A3;
then reconsider y9 = y as Point of T ;
( y9 in O & O c= A9 ) by A3, A4;
then A is a_neighborhood of y9 by URYSOHN1:def 6;
hence o in Int A9 by CONNSP_2:def 1, A1; :: thesis: verum
end;
hence Int A c= Int A9 ; :: thesis: Int A9 c= Int A
now :: thesis: for o being object st o in Int A9 holds
o in Int A
let o be object ; :: thesis: ( o in Int A9 implies o in Int A )
assume A5: o in Int A9 ; :: thesis: o in Int A
then reconsider x = o as Point of T ;
consider O being Subset of T such that
A6: O is open and
A7: x in O and
A8: O c= A9 by A5, CONNSP_2:def 1, URYSOHN1:def 6;
Top2NTop T = NT by FINTOPO7:25;
then reconsider NO = O as open Subset of NT by A6, Lm1;
x in NO by A7;
then reconsider y = x as Point of NT ;
( y in NO & NO c= A ) by A7, A8;
then y is_interior_point_of A by Lm4;
hence o in Int A ; :: thesis: verum
end;
hence Int A9 c= Int A ; :: thesis: verum
end;
hence Int A = Int (NTop2Top A) ; :: thesis: verum