let NT be NTopSpace; :: thesis: for A being Subset of NT holds
( A is open iff Int A = A )
let A be Subset of NT; :: thesis: ( A is open iff Int A = A )

hereby :: thesis: ( Int A = A implies A is open )

assume A1: A is open ; :: thesis: Int A = A
A2: 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 A holds
o in Int A

let o be object ; :: thesis: ( o in A implies o in Int A )
assume A3: o in A ; :: thesis: o in Int A
A in { O where O is open Subset of NT : O c= A } by A1;
hence o in Int A by A2, A3, TARSKI:def 4; :: thesis: verum

end;

then A c= Int A ;
hence Int A = A by Lm15; :: thesis: verum

end;

assume Int A = A ; :: thesis: A is open
hence A is open ; :: thesis: verum