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 A3, PRE_TOPC:def 2;
then ( Q1 c= Q & Q1 in the topology of X1 ) by PRE_TOPC:def 4, XBOOLE_1:17;
hence ( Q1 is open & Q1 c= A1 & p in Q1 ) by A1, A2, A4, PRE_TOPC:def 2, XBOOLE_0:def 4; :: thesis: verum

end;

hence p in Int A1 by TOPS_1:22; :: thesis: verum