let B be Subset of [:X,Y:]; :: according to TOPS_2:def 1 :: thesis: ( not B in Base-Appr A or B is open )

assume B in Base-Appr A ; :: thesis: B is open

then 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 ) ;

hence B is open by Th6; :: thesis: verum

assume B in Base-Appr A ; :: thesis: B is open

then 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 ) ;

hence B is open by Th6; :: thesis: verum