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