let X be Subset of REAL; :: thesis: for r3 being Real holds
( r3 in Cl X iff for O being open Subset of REAL st r3 in O holds
not O /\ X is empty )
let r3 be Real; :: thesis: ( r3 in Cl X iff for O being open Subset of REAL st r3 in O holds
not O /\ X is empty )

hereby :: thesis: ( ( for O being open Subset of REAL st r3 in O holds
not O /\ X is empty ) implies r3 in Cl X )

assume A1: r3 in Cl X ; :: thesis: for O being open Subset of REAL st r3 in O holds
not O /\ X is empty
let O be open Subset of REAL; :: thesis: ( r3 in O implies not O /\ X is empty )
assume that
A2: r3 in O and
A3: O /\ X is empty ; :: thesis: contradiction
O misses X by A3;
then A4: X c= O ` by SUBSET_1:23;
A5: O misses O ` by SUBSET_1:24;
O ` is closed by RCOMP_1:def 5;
then Cl X c= O ` by A4, Th57;
hence contradiction by A1, A2, A5, XBOOLE_0:3; :: thesis: verum

end;

A6: (Cl X) ` is open ;
( X c= Cl X & ((Cl X) `) /\ X c= X ) by Th58, XBOOLE_1:17;
then A7: ((Cl X) `) /\ X c= Cl X ;
((Cl X) `) /\ X c= (Cl X) ` by XBOOLE_1:17;
then A8: ((Cl X) `) /\ X is empty by A7, SUBSET_1:20;
reconsider rr3 = r3 as Element of REAL by XREAL_0:def 1;
assume for O being open Subset of REAL st r3 in O holds
not O /\ X is empty ; :: thesis: r3 in Cl X
then not rr3 in (Cl X) ` by A6, A8;
hence r3 in Cl X by SUBSET_1:29; :: thesis: verum