let X, Y be TopSpace; :: thesis: for A being Subset of [:X,Y:] holds union (Base-Appr A) c= A
let A be Subset of [:X,Y:]; :: thesis: union (Base-Appr A) c= A
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in union (Base-Appr A) or e in A )
assume e in union (Base-Appr A) ; :: thesis: e in A
then consider B being set such that
A1: e in B and
A2: B in Base-Appr A by TARSKI:def 4;
ex X1 being Subset of X ex Y1 being Subset of Y st
( B = [:X1,Y1:] & [:X1,Y1:] c= A & X1 is open & Y1 is open ) by A2;
hence e in A by A1; :: thesis: verum