let T be TopStruct ; :: thesis: for X' being SubSpace of T
for A being Subset of
for A1 being Subset of st A = A1 holds
Cl A1 = (Cl A) /\ ([#] X')
let X' be SubSpace of T; :: thesis: for A being Subset of
for A1 being Subset of st A = A1 holds
Cl A1 = (Cl A) /\ ([#] X')
let A be Subset of ; :: thesis: for A1 being Subset of st A = A1 holds
Cl A1 = (Cl A) /\ ([#] X')
let A1 be Subset of ; :: 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

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

proof

let D1 be Subset of ; :: 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 )
set D3 = D1 /\ ([#] X');
assume A c= D1 ; :: thesis: p in D1
then A5: A1 c= D1 /\ ([#] X') by A1, XBOOLE_1:19;
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;

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 by XBOOLE_0:def 4;

now

let D1 be Subset of ; :: thesis: ( D1 is closed & A1 c= D1 implies p in D1 )
assume D1 is closed ; :: thesis: ( A1 c= D1 implies p in D1 )
then consider D2 being Subset of such that
A8: D2 is closed and
A9: D1 = D2 /\ ([#] X') by Th43;
A10: D2 /\ ([#] X') c= D2 by XBOOLE_1:17;
assume A1 c= D1 ; :: thesis: p in D1
then A c= D2 by A1, A9, A10, XBOOLE_1:1;
then p in D2 by A7, A8, Th45;
hence p in D1 by A6, A9, 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