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