let X be non empty TopSpace; :: thesis: for X1 being SubSpace of X
for A being Subset of X
for A1 being Subset of X1 st A = A1 holds
(Int A) /\ ([#] X1) c= Int A1

let X1 be SubSpace of X; :: thesis: for A being Subset of X
for A1 being Subset of X1 st A = A1 holds
(Int A) /\ ([#] X1) c= Int A1

let A be Subset of X; :: thesis: for A1 being Subset of X1 st A = A1 holds
(Int A) /\ ([#] X1) c= Int A1

let A1 be Subset of X1; :: thesis: ( A = A1 implies (Int A) /\ ([#] X1) c= Int A1 )
assume A1: A = A1 ; :: thesis: (Int A) /\ ([#] X1) c= Int A1
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in (Int A) /\ ([#] X1) or p in Int A1 )
assume A2: p in (Int A) /\ ([#] X1) ; :: thesis: p in Int A1
then p in Int A by XBOOLE_0:def 4;
then consider Q being Subset of X such that
A3: Q is open and
A4: ( Q c= A & p in Q ) by TOPS_1:22;
ex Q1 being Subset of X1 st
( Q1 is open & Q1 c= A1 & p in Q1 )
proof
reconsider Q1 = Q /\ ([#] X1) as Subset of X1 ;
take Q1 ; :: thesis: ( Q1 is open & Q1 c= A1 & p in Q1 )
Q in the topology of X by ;
then ( Q1 c= Q & Q1 in the topology of X1 ) by ;
hence ( Q1 is open & Q1 c= A1 & p in Q1 ) by ; :: thesis: verum
end;
hence p in Int A1 by TOPS_1:22; :: thesis: verum