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

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