let A be Subset of REAL ; :: thesis: for B being Subset of R^1 st A = B holds
Cl A = Cl B
let B be Subset of R^1 ; :: thesis: ( A = B implies Cl A = Cl B )
assume A1: A = B ; :: thesis: Cl A = Cl B
thus Cl A c= Cl B :: according to XBOOLE_0:def 10 :: thesis: Cl B c= Cl A

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in Cl A or a in Cl B )
assume A2: a in Cl A ; :: thesis: a in Cl B
for G being Subset of R^1 st G is open & a in G holds
B meets G

proof

let G be Subset of R^1 ; :: thesis: ( G is open & a in G implies B meets G )
assume that
A3: G is open and
A4: a in G ; :: thesis: B meets G
A5: G in Family_open_set RealSpace by A3, Lm2, PRE_TOPC:def 5;
reconsider H = G as Subset of REAL by TOPMETR:24;
H is open by A5, JORDAN5A:6;
then not A /\ H is empty by A2, A4, PSCOMP_1:38;
hence B meets G by A1, XBOOLE_0:def 7; :: thesis: verum

end;

hence a in Cl B by A2, PRE_TOPC:def 13, TOPMETR:24; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in Cl B or a in Cl A )
assume A6: a in Cl B ; :: thesis: a in Cl A
for O being open Subset of REAL st a in O holds
not O /\ A is empty

proof

let O be open Subset of REAL ; :: thesis: ( a in O implies not O /\ A is empty )
assume A7: a in O ; :: thesis: not O /\ A is empty
reconsider P = O as Subset of R^1 by TOPMETR:24;
P in Family_open_set RealSpace by JORDAN5A:6;
then P is open by Lm2, PRE_TOPC:def 5;
then P meets B by A6, A7, PRE_TOPC:def 13;
hence not O /\ A is empty by A1, XBOOLE_0:def 7; :: thesis: verum

end;

hence a in Cl A by A6, PSCOMP_1:38, TOPMETR:24; :: thesis: verum