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 object ; :: 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
reconsider H = G as Subset of REAL by TOPMETR:17;
G in Family_open_set RealSpace by A3, Lm8;
then H is open by Th5;
then not A /\ H is empty by A2, A4, MEASURE6:63;
hence B meets G by A1; :: thesis: verum
end;
hence a in Cl B by A2, PRE_TOPC:def 7, TOPMETR:17; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Cl B or a in Cl A )
assume A5: 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 A6: a in O ; :: thesis: not O /\ A is empty
reconsider P = O as Subset of R^1 by TOPMETR:17;
P in Family_open_set RealSpace by Th5;
then P is open by Lm8;
then P meets B by A5, A6, PRE_TOPC:def 7;
hence not O /\ A is empty by A1; :: thesis: verum
end;
hence a in Cl A by A5, MEASURE6:63; :: thesis: verum