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

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

thus
union (Base-Appr A) c= A
by Th12; :: thesis: verum
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;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