let NT be NTopSpace; :: thesis: for A being Subset of NT holds Int A = union { O where O is open Subset of NT : O c= A }
let A be Subset of NT; :: thesis: Int A = union { O where O is open Subset of NT : O c= A }
set B = union { O where O is open Subset of NT : O c= A } ;
now :: thesis: ( Int A c= union { O where O is open Subset of NT : O c= A } & union { O where O is open Subset of NT : O c= A } c= Int A )
now :: thesis: for o being object st o in Int A holds
o in union { O where O is open Subset of NT : O c= A }
let o be object ; :: thesis: ( o in Int A implies o in union { O where O is open Subset of NT : O c= A } )
assume o in Int A ; :: thesis: o in union { O where O is open Subset of NT : O c= A }
then consider x being Point of NT such that
A1: o = x and
A2: x is_interior_point_of A ;
consider O being open Subset of NT such that
A3: x in O and
A4: O c= A by A2, Lm4;
O in { O where O is open Subset of NT : O c= A } by A4;
hence o in union { O where O is open Subset of NT : O c= A } by A1, A3, TARSKI:def 4; :: thesis: verum
end;
hence Int A c= union { O where O is open Subset of NT : O c= A } ; :: thesis: union { O where O is open Subset of NT : O c= A } c= Int A
now :: thesis: for o being object st o in union { O where O is open Subset of NT : O c= A } holds
o in Int A
let o be object ; :: thesis: ( o in union { O where O is open Subset of NT : O c= A } implies o in Int A )
assume o in union { O where O is open Subset of NT : O c= A } ; :: thesis: o in Int A
then consider X being set such that
A5: o in X and
A6: X in { O where O is open Subset of NT : O c= A } by TARSKI:def 4;
consider O being open Subset of NT such that
A7: X = O and
A8: O c= A by A6;
reconsider x = o as Point of NT by A5, A7;
x is_interior_point_of A by A5, A7, A8, Lm4;
hence o in Int A ; :: thesis: verum
end;
hence union { O where O is open Subset of NT : O c= A } c= Int A ; :: thesis: verum
end;
hence Int A = union { O where O is open Subset of NT : O c= A } ; :: thesis: verum