let T be TopStruct ; :: thesis: for X' being SubSpace of T
for A being Subset of T
for A1 being Subset of X' st A = A1 holds
Cl A1 = (Cl A) /\ ([#] X')
let X' be SubSpace of T; :: thesis: for A being Subset of T
for A1 being Subset of X' st A = A1 holds
Cl A1 = (Cl A) /\ ([#] X')
let A be Subset of T; :: thesis: for A1 being Subset of X' st A = A1 holds
Cl A1 = (Cl A) /\ ([#] X')
let A1 be Subset of X'; :: thesis: ( A = A1 implies Cl A1 = (Cl A) /\ ([#] X') )
assume A1: A = A1 ; :: thesis: Cl A1 = (Cl A) /\ ([#] X')
for p being set holds
( p in Cl A1 iff p in (Cl A) /\ ([#] X') )

proof

let p be set ; :: thesis: ( p in Cl A1 iff p in (Cl A) /\ ([#] X') )
thus ( p in Cl A1 implies p in (Cl A) /\ ([#] X') ) :: thesis: ( p in (Cl A) /\ ([#] X') implies p in Cl A1 )

proof

assume A2: p in Cl A1 ; :: thesis: p in (Cl A) /\ ([#] X')
A3: for D1 being Subset of T st D1 is closed & A c= D1 holds
p in D1

proof

let D1 be Subset of T; :: thesis: ( D1 is closed & A c= D1 implies p in D1 )
assume A4: D1 is closed ; :: thesis: ( not A c= D1 or p in D1 )
assume A c= D1 ; :: thesis: p in D1
then A5: A1 c= D1 /\ ([#] X') by A1, XBOOLE_1:19;
set D3 = D1 /\ ([#] X');
D1 /\ ([#] X') is closed by A4, Th43;
then p in D1 /\ ([#] X') by A2, A5, Th45;
hence p in D1 by XBOOLE_0:def 4; :: thesis: verum

end;

reconsider DD = Cl A1 as Subset of T by Th39;
p in DD by A2;
then p in Cl A by A3, Th45;
hence p in (Cl A) /\ ([#] X') by A2, XBOOLE_0:def 4; :: thesis: verum

end;

assume A6: p in (Cl A) /\ ([#] X') ; :: thesis: p in Cl A1
then A7: ( p in Cl A & p in [#] X' ) by XBOOLE_0:def 4;

now

let D1 be Subset of X'; :: thesis: ( D1 is closed & A1 c= D1 implies p in D1 )
assume A8: D1 is closed ; :: thesis: ( A1 c= D1 implies p in D1 )
assume A9: A1 c= D1 ; :: thesis: p in D1
consider D2 being Subset of T such that
A10: D2 is closed and
A11: D1 = D2 /\ ([#] X') by A8, Th43;
D2 /\ ([#] X') c= D2 by XBOOLE_1:17;
then A c= D2 by A1, A9, A11, XBOOLE_1:1;
then p in D2 by A7, A10, Th45;
hence p in D1 by A6, A11, XBOOLE_0:def 4; :: thesis: verum

end;

hence p in Cl A1 by A6, Th45; :: thesis: verum

end;

hence Cl A1 = (Cl A) /\ ([#] X') by TARSKI:2; :: thesis: verum