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 )

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

hence
p in Int A1
by TOPS_1:22; :: thesis: verum
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;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