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
for p being set st p in (Int A) /\ ([#] X1) holds
p in Int A1

proof

let p be set ; :: thesis: ( p in (Int A) /\ ([#] X1) implies p in Int A1 )
assume A2: p in (Int A) /\ ([#] X1) ; :: thesis: p in Int A1
then ( p in Int A & p in [#] X1 ) by XBOOLE_0:def 4;
then consider Q being Subset of X such that
A3: Q is open and
A4: Q c= A and
A5: p in Q by TOPS_1:54;
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 )
A6: Q1 c= Q by XBOOLE_1:17;
Q in the topology of X by A3, PRE_TOPC:def 5;
then Q1 in the topology of X1 by PRE_TOPC:def 9;
hence ( Q1 is open & Q1 c= A1 & p in Q1 ) by A1, A2, A4, A5, A6, PRE_TOPC:def 5, XBOOLE_0:def 4, XBOOLE_1:1; :: thesis: verum

end;

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

end;

hence (Int A) /\ ([#] X1) c= Int A1 by TARSKI:def 3; :: thesis: verum