let X, Y be TopSpace; 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:]; ( A c= B implies Base-Appr A c= Base-Appr B )
assume A1:
A c= B
; Base-Appr A c= Base-Appr B
let e be object ; TARSKI:def 3 ( not e in Base-Appr A or e in Base-Appr B )
assume
e in Base-Appr A
; 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; verum