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: (T \/ (Cl T)) /\ (T \/ (Cl (T `))) = (Cl T) /\ (T \/ (Cl (T `))) by PRE_TOPC:18, XBOOLE_1:12;
T \/ ((Cl T) \ T) c= T \/ ((Cl T) /\ (Cl (T `)))
proof
let x be object ; :: 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 x99 = x as Point of GX ;
( x99 in T or x99 in (Cl T) \ T ) by A2, XBOOLE_0:def 3;
then A3: ( x99 in T or ( x99 in Cl T & x99 in T ` ) ) by XBOOLE_0:def 5;
T ` c= Cl (T `) by PRE_TOPC:18;
then ( x99 in T or x99 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:18, 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; :: thesis: verum