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)
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in A " (Int G) or e in Int (A " G) )
A1: A " (Int G) c= A " G by RELAT_1:143, TOPS_1:16;
[#] Y <> {} ;
then A2: A " (Int G) is open by TOPS_2:43;
assume e in A " (Int G) ; :: thesis: e in Int (A " G)
hence e in Int (A " G) by A2, A1, TOPS_1:22; :: thesis: verum