let GX be TopStruct ; :: thesis: for T being Subset of holds Cl T = T \/ (Fr T)
let T be Subset of ; :: thesis: Cl T = T \/ (Fr T)
A1: (T \/ (Cl T)) /\ (T \/ (Cl (T ` ))) = (Cl T) /\ (T \/ (Cl (T ` ))) by PRE_TOPC:48, XBOOLE_1:12;
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 ;
( 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;

then A4: Cl T c= T \/ (Fr T) by PRE_TOPC:48, XBOOLE_1:45;
T \/ (Fr T) = (T \/ (Cl T)) /\ (T \/ (Cl (T ` ))) by XBOOLE_1:24;
then T \/ (Fr T) c= Cl T by A1, XBOOLE_1:17;
hence Cl T = T \/ (Fr T) by A4, XBOOLE_0:def 10; :: thesis: verum