let T be TopStruct ; :: thesis: for X9 being SubSpace of T
for A being Subset of T
for A1 being Subset of X9 st A = A1 holds
Cl A1 = (Cl A) /\ ([#] X9)
let X9 be SubSpace of T; :: thesis: for A being Subset of T
for A1 being Subset of X9 st A = A1 holds
Cl A1 = (Cl A) /\ ([#] X9)
let A be Subset of T; :: thesis: for A1 being Subset of X9 st A = A1 holds
Cl A1 = (Cl A) /\ ([#] X9)
let A1 be Subset of X9; :: thesis: ( A = A1 implies Cl A1 = (Cl A) /\ ([#] X9) )
assume A1: A = A1 ; :: thesis: Cl A1 = (Cl A) /\ ([#] X9)
for p being object holds
( p in Cl A1 iff p in (Cl A) /\ ([#] X9) )
proof
let p be object ; :: thesis: ( p in Cl A1 iff p in (Cl A) /\ ([#] X9) )
thus ( p in Cl A1 implies p in (Cl A) /\ ([#] X9) ) :: thesis: ( p in (Cl A) /\ ([#] X9) implies p in Cl A1 )
proof
reconsider DD = Cl A1 as Subset of T by Th11;
assume A2: p in Cl A1 ; :: thesis: p in (Cl A) /\ ([#] X9)
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 )
set D3 = D1 /\ ([#] X9);
assume A c= D1 ; :: thesis: p in D1
then A5: A1 c= D1 /\ ([#] X9) by A1, XBOOLE_1:19;
D1 /\ ([#] X9) is closed by A4, Th13;
then p in D1 /\ ([#] X9) by A2, A5, Th15;
hence p in D1 by XBOOLE_0:def 4; :: thesis: verum
end;
p in DD by A2;
then p in Cl A by A3, Th15;
hence p in (Cl A) /\ ([#] X9) by A2, XBOOLE_0:def 4; :: thesis: verum
end;
assume A6: p in (Cl A) /\ ([#] X9) ; :: thesis: p in Cl A1
then A7: p in Cl A by XBOOLE_0:def 4;
now :: thesis: for D1 being Subset of X9 st D1 is closed & A1 c= D1 holds
p in D1
let D1 be Subset of X9; :: 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 T such that
A8: D2 is closed and
A9: D1 = D2 /\ ([#] X9) by Th13;
A10: D2 /\ ([#] X9) c= D2 by XBOOLE_1:17;
assume A1 c= D1 ; :: thesis: p in D1
then A c= D2 by A1, A9, A10;
then p in D2 by A7, A8, Th15;
hence p in D1 by A6, A9, XBOOLE_0:def 4; :: thesis: verum
end;
hence p in Cl A1 by A6, Th15; :: thesis: verum
end;
hence Cl A1 = (Cl A) /\ ([#] X9) by TARSKI:2; :: thesis: verum