let X, Y be non empty TopSpace; :: thesis: for A being continuous Function of X,Y
for G being Subset of Y holds A " (Int G) c= Int (A " G)
let A be continuous Function of X,Y; :: thesis: for G being Subset of Y holds A " (Int G) c= Int (A " G)
let G be Subset of Y; :: thesis: A " (Int G) c= Int (A " G)
[#] Y <> {} ;
then A1: A " (Int G) is open by TOPS_2:55;
let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in A " (Int G) or e in Int (A " G) )
assume A2: e in A " (Int G) ; :: thesis: e in Int (A " G)
A " (Int G) c= A " G by RELAT_1:178, TOPS_1:44;
hence e in Int (A " G) by A1, A2, TOPS_1:54; :: thesis: verum