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