let X be RealNormSpace; :: thesis: for V being Subset of (TopSpaceNorm X)
for V1 being Subset of (LinearTopSpaceNorm X) st V = V1 holds
Cl V = Cl V1
let V be Subset of (TopSpaceNorm X); :: thesis: for V1 being Subset of (LinearTopSpaceNorm X) st V = V1 holds
Cl V = Cl V1
let V1 be Subset of (LinearTopSpaceNorm X); :: 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 (LinearTopSpaceNorm X) st D1 is closed & V1 c= D1 holds
z in D1
proof
let D1 be Subset of (LinearTopSpaceNorm X); :: 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 (TopSpaceNorm X) by NORMSP_2:def 4;
D0 is closed by A4, NORMSP_2:32;
then A5: D2 is closed by NORMSP_2:15;
assume V1 c= D1 ; :: thesis: z in D1
hence z in D1 by A1, A2, A5, PRE_TOPC:15; :: thesis: verum
end;
z in the carrier of X by A2;
then z in the carrier of (LinearTopSpaceNorm X) by NORMSP_2:def 4;
hence z in Cl V1 by A3, PRE_TOPC:15; :: 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 (TopSpaceNorm X) st D1 is closed & V c= D1 holds
z in D1
proof
let D1 be Subset of (TopSpaceNorm X); :: 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 (LinearTopSpaceNorm X) by NORMSP_2:def 4;
D0 is closed by A8, NORMSP_2:15;
then A9: D2 is closed by NORMSP_2:32;
assume V c= D1 ; :: thesis: z in D1
hence z in D1 by A1, A6, A9, PRE_TOPC:15; :: thesis: verum
end;
z in the carrier of (LinearTopSpaceNorm X) by A6;
then z in the carrier of (TopSpaceNorm X) by NORMSP_2:def 4;
hence z in Cl V by A7, PRE_TOPC:15; :: thesis: verum