let GX be TopStruct ; :: thesis: for T being Subset of GX holds Fr T = ((Cl (T ` )) /\ T) \/ ((Cl T) \ T)
let T be Subset of GX; :: thesis: Fr T = ((Cl (T ` )) /\ T) \/ ((Cl T) \ T)
for x being set holds
( x in Fr T iff x in ((Cl (T ` )) /\ T) \/ ((Cl T) \ T) )

proof

let x be set ; :: thesis: ( x in Fr T iff x in ((Cl (T ` )) /\ T) \/ ((Cl T) \ T) )
A1: T c= Cl T by PRE_TOPC:48;
A2: T ` c= Cl (T ` ) by PRE_TOPC:48;
thus ( x in Fr T implies x in ((Cl (T ` )) /\ T) \/ ((Cl T) \ T) ) :: thesis: ( x in ((Cl (T ` )) /\ T) \/ ((Cl T) \ T) implies x in Fr T )

proof

assume A3: x in Fr T ; :: thesis: x in ((Cl (T ` )) /\ T) \/ ((Cl T) \ T)
then reconsider x'' = x as Point of GX ;
( ( x'' in Cl T & x'' in Cl (T ` ) & x'' in T ) or ( x'' in Cl T & x'' in Cl (T ` ) & x'' in T ` ) ) by A3, SUBSET_1:50, XBOOLE_0:def 4;
then ( x'' in (Cl (T ` )) /\ T or ( not x'' in T & x'' in Cl T ) ) by XBOOLE_0:def 4;
then ( x'' in (Cl (T ` )) /\ T or x'' in (Cl T) \ T ) by XBOOLE_0:def 5;
hence x in ((Cl (T ` )) /\ T) \/ ((Cl T) \ T) by XBOOLE_0:def 3; :: thesis: verum

end;

thus ( x in ((Cl (T ` )) /\ T) \/ ((Cl T) \ T) implies x in Fr T ) :: thesis: verum

proof

assume A4: x in ((Cl (T ` )) /\ T) \/ ((Cl T) \ T) ; :: thesis: x in Fr T
then reconsider x'' = x as Point of GX ;
( x'' in (Cl (T ` )) /\ T or x'' in (Cl T) \ T ) by A4, XBOOLE_0:def 3;
then ( ( x'' in Cl (T ` ) & x'' in T ) or ( x'' in Cl T & not x'' in T ) ) by XBOOLE_0:def 4, XBOOLE_0:def 5;
then ( ( x'' in Cl (T ` ) & x'' in T ) or ( x'' in Cl T & x'' in T ` ) ) by SUBSET_1:50;
hence x in Fr T by A1, A2, XBOOLE_0:def 4; :: thesis: verum

end;

end;

hence Fr T = ((Cl (T ` )) /\ T) \/ ((Cl T) \ T) by TARSKI:2; :: thesis: verum