let X be RealNormSpace; :: thesis: for V being Subset of ()
for V1 being Subset of st V = V1 holds
Cl V = Cl V1

let V be Subset of (); :: thesis: for V1 being Subset of st V = V1 holds
Cl V = Cl V1

let V1 be Subset of ; :: thesis: ( V = V1 implies Cl V = Cl V1 )
assume A1: V = V1 ; :: thesis: Cl V = Cl V1
thus Cl V c= Cl V1 :: according to XBOOLE_0:def 10 :: thesis: Cl V1 c= Cl V
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Cl V or z in Cl V1 )
assume A2: z in Cl V ; :: thesis: z in Cl V1
A3: for D1 being Subset of st D1 is closed & V1 c= D1 holds
z in D1
proof
let D1 be Subset of ; :: thesis: ( D1 is closed & V1 c= D1 implies z in D1 )
assume A4: D1 is closed ; :: thesis: ( not V1 c= D1 or z in D1 )
reconsider D0 = D1 as Subset of X by NORMSP_2:def 4;
reconsider D2 = D1 as Subset of () by NORMSP_2:def 4;
D0 is closed by ;
then A5: D2 is closed by NORMSP_2:15;
assume V1 c= D1 ; :: thesis: z in D1
hence z in D1 by ; :: thesis: verum
end;
z in the carrier of X by A2;
then z in the carrier of by NORMSP_2:def 4;
hence z in Cl V1 by ; :: thesis: verum
end;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Cl V1 or z in Cl V )
assume A6: z in Cl V1 ; :: thesis: z in Cl V
A7: for D1 being Subset of () st D1 is closed & V c= D1 holds
z in D1
proof
let D1 be Subset of (); :: thesis: ( D1 is closed & V c= D1 implies z in D1 )
assume A8: D1 is closed ; :: thesis: ( not V c= D1 or z in D1 )
reconsider D0 = D1 as Subset of X ;
reconsider D2 = D1 as Subset of by NORMSP_2:def 4;
D0 is closed by ;
then A9: D2 is closed by NORMSP_2:32;
assume V c= D1 ; :: thesis: z in D1
hence z in D1 by ; :: thesis: verum
end;
z in the carrier of by A6;
then z in the carrier of () by NORMSP_2:def 4;
hence z in Cl V by ; :: thesis: verum