let X, Y be TopSpace; :: thesis: for A being Subset of holds Int A = union (Base-Appr A)
let A be Subset of ; :: thesis: Int A = union (Base-Appr A)
( Int A = union (Base-Appr (Int A)) & Base-Appr (Int A) c= Base-Appr A ) by Th52, Th54, TOPS_1:44;
hence Int A c= union (Base-Appr A) by ZFMISC_1:95; :: according to XBOOLE_0:def 10 :: thesis: union (Base-Appr A) c= Int A
union (Base-Appr A) is open by Th51, TOPS_2:26;
hence union (Base-Appr A) c= Int A by Th53, TOPS_1:56; :: thesis: verum