let GX be TopStruct ; :: thesis: for T being Subset of GX holds Cl T = T \/ (Fr T)
let T be Subset of GX; :: thesis: Cl T = T \/ (Fr T)
A1: Cl T c= T \/ (Fr T)

proof

T \/ ((Cl T) \ T) c= T \/ ((Cl T) /\ (Cl (T ` )))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in T \/ ((Cl T) \ T) or x in T \/ ((Cl T) /\ (Cl (T ` ))) )
assume A2: x in T \/ ((Cl T) \ T) ; :: thesis: x in T \/ ((Cl T) /\ (Cl (T ` )))
then reconsider x'' = x as Point of GX ;
( x'' in T or x'' in (Cl T) \ T ) by A2, XBOOLE_0:def 3;
then A3: ( x'' in T or ( x'' in Cl T & x'' in T ` ) ) by XBOOLE_0:def 5;
T ` c= Cl (T ` ) by PRE_TOPC:48;
then ( x'' in T or x'' in (Cl T) /\ (Cl (T ` )) ) by A3, XBOOLE_0:def 4;
hence x in T \/ ((Cl T) /\ (Cl (T ` ))) by XBOOLE_0:def 3; :: thesis: verum

end;

hence Cl T c= T \/ (Fr T) by PRE_TOPC:48, XBOOLE_1:45; :: thesis: verum

end;

T \/ (Fr T) c= Cl T

proof

A4: T \/ (Fr T) = (T \/ (Cl T)) /\ (T \/ (Cl (T ` ))) by XBOOLE_1:24;
(T \/ (Cl T)) /\ (T \/ (Cl (T ` ))) = (Cl T) /\ (T \/ (Cl (T ` ))) by PRE_TOPC:48, XBOOLE_1:12;
hence T \/ (Fr T) c= Cl T by A4, XBOOLE_1:17; :: thesis: verum

end;

hence Cl T = T \/ (Fr T) by A1, XBOOLE_0:def 10; :: thesis: verum