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

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