let X, Y be TopSpace; :: thesis: for A being Subset of [:X,Y:] st A is open holds
A = union (Base-Appr A)
let A be Subset of [:X,Y:]; :: thesis: ( A is open implies A = union (Base-Appr A) )
assume A is open ; :: thesis: A = union (Base-Appr A)
then consider B being Subset-Family of [:X,Y:] such that
A1: A = union B and
A2: for e being set st e in B holds
ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) by Th5;
thus A c= union (Base-Appr A) :: according to XBOOLE_0:def 10 :: thesis: union (Base-Appr A) c= A

proof

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

end;

thus union (Base-Appr A) c= A by Th12; :: thesis: verum