let X, Y be TopSpace; :: thesis: for A being Subset of [:X,Y:] holds Int A = union (Base-Appr A)
let A be Subset of [:X,Y:]; :: thesis: Int A = union (Base-Appr A)
( Int A = union (Base-Appr (Int A)) & Base-Appr (Int A) c= Base-Appr A ) by Th11, Th13, TOPS_1:16;
hence Int A c= union (Base-Appr A) by ZFMISC_1:77; :: according to XBOOLE_0:def 10 :: thesis: union (Base-Appr A) c= Int A
union (Base-Appr A) is open by TOPS_2:19;
hence union (Base-Appr A) c= Int A by Th12, TOPS_1:24; :: thesis: verum