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, XBOOLE_0:def 7;
then A4: X c= O ` by SUBSET_1:43;
O ` is closed by RCOMP_1:def 5;
then A5: Cl X c= O ` by A4, Th32;
O misses O ` by SUBSET_1:44;
hence contradiction by A1, A2, A5, XBOOLE_0:3; :: thesis: verum

end;

assume A6: for O being open Subset of REAL st r3 in O holds
not O /\ X is empty ; :: thesis: r3 in Cl X
((Cl X) ` ) ` = Cl X ;
then A7: (Cl X) ` is open by RCOMP_1:def 5;
A8: X c= Cl X by Th33;
((Cl X) ` ) /\ X c= X by XBOOLE_1:17;
then ( ((Cl X) ` ) /\ X c= Cl X & ((Cl X) ` ) /\ X c= (Cl X) ` ) by A8, XBOOLE_1:1, XBOOLE_1:17;
then ((Cl X) ` ) /\ X is empty by SUBSET_1:40;
then not r3 in (Cl X) ` by A6, A7;
hence r3 in Cl X by SUBSET_1:50; :: thesis: verum