let NT be NTopSpace; :: thesis: for A being Subset of NT
for B being open Subset of NT st B c= A holds
B c= Int A
let A be Subset of NT; :: thesis: for B being open Subset of NT st B c= A holds
B c= Int A
let B be open Subset of NT; :: thesis: ( B c= A implies B c= Int A )
set C = { O where O is open Subset of NT : O c= A } ;
assume B c= A ; :: thesis: B c= Int A
then A1: B in { O where O is open Subset of NT : O c= A } ;
Int A = union { O where O is open Subset of NT : O c= A } by Lm5;
hence B c= Int A by A1, TARSKI:def 4; :: thesis: verum