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

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