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

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

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

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 V1 or z in Cl V )
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

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;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

z in the carrier of X
by A2;
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;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

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

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

z in the carrier of (LinearTopSpaceNorm X)
by A6;
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;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

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