let NT be NTopSpace; :: thesis: for A being Subset of NT
for x being Point of NT holds
( x is_interior_point_of A iff ex O being open Subset of NT st
( x in O & O c= A ) )
let A be Subset of NT; :: thesis: for x being Point of NT holds
( x is_interior_point_of A iff ex O being open Subset of NT st
( x in O & O c= A ) )
let x be Point of NT; :: thesis: ( x is_interior_point_of A iff ex O being open Subset of NT st
( x in O & O c= A ) )
now :: thesis: ( ex O being open Subset of NT st
( x in O & O c= A ) implies x is_interior_point_of A )
assume ex O being open Subset of NT st
( x in O & O c= A ) ; :: thesis: x is_interior_point_of A
then consider O being open Subset of NT such that
A1: x in O and
A2: O c= A ;
( O in U_FMT x & U_FMT x is Filter of the carrier of NT ) by A1, FINTOPO7:def 1;
then A in U_FMT x by A2, CARD_FIL:def 1;
hence x is_interior_point_of A by FINTOPO7:def 5; :: thesis: verum
end;
hence ( x is_interior_point_of A iff ex O being open Subset of NT st
( x in O & O c= A ) ) by FINTOPO7:15; :: thesis: verum