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)
A1: Int A = union (Base-Appr (Int A)) by Th54;
Base-Appr (Int A) c= Base-Appr A by Th52, TOPS_1:44;
hence Int A c= union (Base-Appr A) by A1, 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